我想编写一个函数,它接受一个字符串并返回一个char列表.这是一个函数,但我认为它不是我想做的(我想取一个字符串并返回一个字符列表).
let rec string_to_char_list s =
match s with
| "" -> []
| n -> string_to_char_list n
我有一个功能PolyInterpretation(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html)
Definition PolyInterpretation := forall f : Sig, poly (arity f).
和模块签名TPolyInt(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html)
Module Type TPolyInt.
Parameter sig : Signature.
Parameter trsInt : PolyInterpretation sig.
Parameter trsInt_wm : PolyWeakMonotone trsInt.
End TPolyInt.
Module PolyInt (Export PI : TPolyInt).
然后在我的文件中rainbow.v,我定义了一个TPolyInt_imp使用仿函数的模块目的PolyInt
Module TPolyInt_imp.
Variable arity : symbol -> nat.
Variable l : list {g : symbol & poly (arity f).
Definition sig := Sig arity.
Definition trsInt f := fun_of_pairs_list …let undefined = ["string"; ""; "string"; "boolean";"";"innermost"]
我有一个列表,我想编写一个函数,返回一个没有重复和空字符串列表的列表.例如,undefined上面的列表将返回:
["string"; "boolean"; "innermost"]
我写这个函数它为我返回没有重复,但我怎么能添加测试空字符串的条件.
let rec uniquify = function
| [] -> []
| x::xs -> x :: uniquify (List.filter ((<>) x) xs)
非常感谢你
编辑
Require Import Bool List ZArith.
Variable A: Type.
Inductive error :=
| Todo.
Inductive result (A : Type) : Type :=
Ok : A -> result A | Ko : error -> result A.
Variable bool_of_result : result A -> bool.
Variable rules : Type.
Variable boolean : Type.
Variable positiveInteger : Type.
Variable OK: result unit.
Definition dps := rules.
Inductive dpProof :=
| DpProof_depGraphProc : list
(dps * boolean * option (list positiveInteger) * option dpProof) -> …module type Arity =
sig
val arity : nat (* in my real code it has another type *)
end
module S =
functor (A : Arity) -> struct
let check = ...
end
我想check在S没有实现签名的情况下使用函子内部的函数Arity.我读了一流的模块,但仍然不明白如何编写它(在实践中).这是我的草案代码:
let A = has type of (module Arity)
然后
let M = S (A)
然后我可以调用check函数
M.check
我试过了:
let f arity = (module (val arity : Arity) : Arity)
它返回: val f : (module Arity) -> (module Arity) …
我有一个问题: Record和Definition
我有这个定义:
Definition rule := term -> term.
我为它写了一个布尔函数.
Definition beq_rule a b := beq_term a && beq_term b.
哪里 beq_term : term -> term -> bool.
所以我的beq_rule实际定义返回的确切类型beq_term不是我想要的.我希望它为我返回一个类型: rule -> rule -> bool.
所以我改变了规则的定义Record:
Record rule := mkRule {lhs : term; rhs : term}.
和
Definition beq_rule (a b : rule) : bool :=
beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).
我的问题是:
1)我的第一次rule使用Definition和另一次使用之间有什么不同 …
我正在使用big_int类型.我查看了OCaml的图书馆Pervasives.
例如:in Int32
let t = 5l
Printf.printf "%ld" t
如何定义t以及%?d如果我要声明它是big_int哪个？
我有一个函数计算列表到布尔矩阵,其中num_of_name: 'a list -> 'a -> int:返回列表中元素的位置.
1)我想 mat_of_dep_rel : 'a list -> bool array array.
我的问题是,从第一个List.iter它应该采取一个列表,l而不是一个空列表[].但如果我返回l而不是[],它会给我一个类型:('a * 'a list) list -> boolean array array.这不是我想要的.
我想知道怎么回来 mat_of_dep_rel: 'a list -> bool array array?
let mat_of_dep_rel l =
let n = List.length l in
let m = Array.make_matrix n n false in
List.iter (fun (s, ss) ->
let i = num_of_name ss s in
List.iter (fun t …有什么区别
if mi.(j) = false && m.(j).(i) = false
和
if not (mi.(j) && m.(j).(i))
因为我认为它具有相同的含义,但是当我运行代码时,它给了我一个不同的答案.
我有3个文件：
1）cpf0.ml
type string = char list
type url = string
type var = string
type name = string
type symbol =
| Symbol_name of name
2）problem.ml:
type symbol =
| Ident of string
3）test.ml
open Problem;;
open Cpf0;;
let symbol b = function
| Symbol_name n -> Ident n
当我结合时test.ml：ocamlc -c test.ml. 我收到一个错误：
该表达式的类型为 Cpf0.name = char list，但表达式应为字符串类型
你能帮我改正吗？非常感谢
编辑：谢谢您的回答。我想详细解释一下这 3 个文件：因为我正在 Coq 中提取到 Ocaml 类型：cpf0.ml生成自
cpf.v：
Require …