pp.cmi: ast.cmi
-disambiguate.cmi: ast.cmi disambiguate_struct.cmo disambiguate_types.cmi
+disambiguate.cmi: ast.cmi disambiguate_types.cmi
parser.cmi: ast.cmi
+disambiguate_types.cmo: disambiguate_types.cmi
+disambiguate_types.cmx: disambiguate_types.cmi
pp.cmo: ast.cmi pp.cmi
pp.cmx: ast.cmi pp.cmi
macro.cmo: macro.cmi
macro.cmx: macro.cmi
lexer.cmo: macro.cmi lexer.cmi
lexer.cmx: macro.cmx lexer.cmi
-disambiguate_struct.cmo: disambiguate_types.cmi
-disambiguate_struct.cmx: disambiguate_types.cmi
parser.cmo: ast.cmi lexer.cmi parser.cmi
parser.cmx: ast.cmi lexer.cmx parser.cmi
-disambiguate.cmo: ast.cmi disambiguate_struct.cmo disambiguate_types.cmi \
- parser.cmi disambiguate.cmi
-disambiguate.cmx: ast.cmi disambiguate_struct.cmx disambiguate_types.cmi \
- parser.cmx disambiguate.cmi
-logic_notation.cmo: ast.cmi parser.cmi
-logic_notation.cmx: ast.cmi parser.cmx
-arit_notation.cmo: ast.cmi parser.cmi
-arit_notation.cmx: ast.cmi parser.cmx
+disambiguate.cmo: ast.cmi disambiguate_types.cmi parser.cmi disambiguate.cmi
+disambiguate.cmx: ast.cmi disambiguate_types.cmx parser.cmx disambiguate.cmi
+logic_notation.cmo: ast.cmi disambiguate.cmi parser.cmi
+logic_notation.cmx: ast.cmi disambiguate.cmx parser.cmx
+arit_notation.cmo: ast.cmi disambiguate.cmi parser.cmi
+arit_notation.cmx: ast.cmi disambiguate.cmx parser.cmx
ast.mli pp.mli macro.mli lexer.mli disambiguate.mli parser.mli \
disambiguate_types.mli
IMPLEMENTATION_FILES = \
- pp.ml macro.ml lexer.ml disambiguate_struct.ml parser.ml \
+ disambiguate_types.ml \
+ pp.ml macro.ml lexer.ml parser.ml \
disambiguate.ml \
$(patsubst %,%_notation.ml,$(NOTATIONS)) \
disambiguate_types.cmi: disambiguate_types.mli
$(OCAMLC) -c -rectypes $<
+disambiguate_types.cmo: disambiguate_types.ml disambiguate_types.cmi
+ $(OCAMLC) -c -rectypes $<
open Ast
open Parser
+(*
+let i = ref max_int
+let get_i () = decr i; !i
+*)
+
EXTEND
term: LEVEL "add"
[
[ t1 = term; SYMBOL "+"; t2 = term ->
- return_term loc (Appl_symbol ("plus", [t1; t2]))
+ return_term loc (Appl_symbol ("plus", 0, [t1; t2]))
| t1 = term; SYMBOL "-"; t2 = term ->
- return_term loc (Appl_symbol ("minus", [t1; t2]))
+ return_term loc (Appl_symbol ("minus", 0, [t1; t2]))
]
];
term: LEVEL "mult"
[
[ t1 = term; SYMBOL "*"; t2 = term ->
- return_term loc (Appl_symbol ("times", [t1; t2]))
+ return_term loc (Appl_symbol ("times", 0, [t1; t2]))
| t1 = term; SYMBOL "/"; t2 = term ->
- return_term loc (Appl_symbol ("div", [t1; t2]))
+ return_term loc (Appl_symbol ("div", 0, [t1; t2]))
]
];
term: LEVEL "inv"
[
- [ SYMBOL "-"; t = term -> return_term loc (Appl_symbol ("uminus", [t])) ]
+ [ SYMBOL "-"; t = term ->
+ return_term loc (Appl_symbol ("uminus", 0, [t]))
+ ]
];
END
+
+let _ =
+ Disambiguate.add_num_choice
+ ("natural number",
+ (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
+ Disambiguate.add_num_choice
+ ("real number",
+ (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
+ Disambiguate.add_symbol_choice "plus"
+ ("natural plus",
+ (fun env _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise Disambiguate.Invalid_choice
+ in
+ Cic.Appl [ HelmLibraryObjects.Peano.plus; t1; t2 ]));
+ Disambiguate.add_symbol_choice "plus"
+ ("real plus",
+ (fun env _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise Disambiguate.Invalid_choice
+ in
+ Cic.Appl [ HelmLibraryObjects.Reals.rplus; t1; t2 ]));
+
| LocatedTerm of location * term
| Appl of term list
- | Appl_symbol of string * term list
+ | Appl_symbol of string * int * term list (* literal, args, instance *)
| Binder of binder_kind * Cic.name * term option * term
(* kind, name, type, body *)
| Case of term * string * term option * (case_pattern * term) list
| LetIn of string * term * term (* name, body, where *)
| LetRec of induction_kind * (string * term * term option * int) list * term
(* (name, body, type, decreasing argument) list, where *)
- | Ident of string * subst list
+ | Ident of string * subst list (* literal, substitutions *)
| Meta of int * meta_subst list
- | Num of string
+ | Num of string * int (* literal, instance *)
| Sort of sort_kind
and meta_subst = term option
* http://helm.cs.unibo.it/
*)
-open Disambiguate_struct
open Disambiguate_types
-let debug = true
-let debug_print = if debug then prerr_endline else ignore
+exception Invalid_choice
+exception No_choices of domain_item
+exception NoWellTypedInterpretation
-type interpretation_domain = Domain.t
-type domain_and_interpretation = interpretation_domain * interpretation
+ (** raised when an environment is not enough informative to decide *)
+exception Try_again
-let string_of_interpretation_domain_item = function
- | Id s -> "ID " ^ s
- | Symbol (s, i) -> "SYMBOL " ^ s ^ " " ^ string_of_int i
- | Num (s, i) -> "NUM " ^ s ^ " " ^ string_of_int i
+let debug = true
+let debug_print = if debug then prerr_endline else ignore
let descr_of_domain_item = function
| Id s -> s
| Symbol (s, _) -> s
- | Num (s, _) -> s
-
-let rec build_natural =
- function
- | 0 -> HelmLibraryObjects.Datatypes.zero
- | n -> Cic.Appl [ HelmLibraryObjects.Datatypes.succ; (build_natural (n - 1)) ]
-
-exception Invalid_choice
+ | Num i -> string_of_int i
-let symbol_choices: (string, interpretation_codomain_item list) Hashtbl.t = Hashtbl.create 1023
-let _ =
- Hashtbl.add symbol_choices "eq"
- [ ("Leibnitz's equality",
- (fun interp args ->
- let t1, t2 =
- match args with
- | [t1; t2] -> t1, t2
- | _ -> raise Invalid_choice
- in
- Cic.Appl [
- Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
- Cic.Implicit; t1; t2
- ])) ]
-(*
-let add_symbol_choice = Hashtbl.add symbol_choices
-let add_symbol_choices symbol = List.iter (add_symbol_choice symbol)
-*)
-let num_choices =
- ref [
- "natural number",
- (fun num ->
- let num = int_of_string num in
- assert (num >= 0);
- build_natural num)
- ]
+let symbol_choices = Hashtbl.create 1023
+let num_choices = ref []
-let add_num_choice choice =
- num_choices := choice :: !num_choices
+let add_symbol_choice symbol codomain_item =
+ let current_choices =
+ try
+ Hashtbl.find symbol_choices symbol
+ with Not_found -> []
+ in
+ Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices)
+let add_num_choice choice = num_choices := choice :: !num_choices
type test_result =
| Ok of Cic.term * Cic.metasenv
| CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
(* TODO remove this case as soon as refine is fully implemented *)
(try
+ debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term));
let term' = CicTypeChecker.type_of_aux' metasenv context term in
Ok (term',metasenv)
- with _ -> Ko)
+(* with _ -> Ko) *)
+ with _ -> Uncertain)
| CicRefine.Uncertain _ ->
debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
Uncertain
with
| Invalid_argument _ -> raise (UriManager.IllFormedUri uri)
-module Make (C: Callbacks) =
- struct
- exception NoWellTypedInterpretation
-
- let choices_of_id mqi_handle id =
- let query = MQueryGenerator.locate id in
- let result = MQueryInterpreter.execute mqi_handle query in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- C.output_html (`Msg (`T "Locate query:"));
- MQueryUtil.text_of_query
- (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
- "" query;
- C.output_html (`Msg (`T "Result:"));
- MQueryUtil.text_of_result
- (fun s -> C.output_html (`Msg (`T s))) "" result;
- let uris' =
- match uris with
- | [] ->
- [UriManager.string_of_uri (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
- | [uri] -> [uri]
- | _ ->
- C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
- ~ok:"Try every selection." ~enable_button_for_non_vars:true
- ~title:"Ambiguous input." ~id
- ~msg: ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- uris
- in
- List.map (fun uri -> (uri, term_of_uri uri)) uris'
-
- let disambiguate_input
- mqi_handle context metasenv parser_dom parser_mk_term
- (current_dom, current_interpretation)
- =
- debug_print "NEW DISAMBIGUATE INPUT";
- let todo_dom = Domain.diff parser_dom current_dom in
- (* (1) for each item in todo_dom we get the associated list of choices *)
- let id_choices = Hashtbl.create 1023 in
- let _ =
- Domain.iter
- (function
- | Id id ->
- (* pairs <description, term> *)
- let choices = choices_of_id mqi_handle id in
- debug_print (sprintf
- "CHOICES_OF_ID di %s ha restituito %d scelte"
- id (List.length choices));
- Hashtbl.add id_choices id choices
- | _ -> assert false)
- (Domain.filter (function Id _ -> true | _ -> false) todo_dom)
- in
- (* (2) lookup function for any item (Id/Symbol/Num) *)
- let lookup_choices item =
- try
- (match item with
- | Id id ->
- let choices = Hashtbl.find id_choices id in
- List.map (fun (descr, term) -> (descr, fun _ _ -> term)) choices
- | Symbol (symb, _) -> Hashtbl.find symbol_choices symb
- | Num (num, _) ->
- List.map
- (fun (descr, f) -> (descr, let term = f num in fun _ _ -> term))
- !num_choices)
- with Not_found -> assert false
- in
- (* (3) test an interpretation filling with meta uninterpreted identifiers
- *)
- let test_interpretation current_interpretation todo_dom =
- let filled_interpretation =
- Domain.fold
- (fun item' interpretation ->
- fun item ->
- if item = item' then
- "Implicit", fun _ _ -> Cic.Implicit
- else
- interpretation item)
- todo_dom current_interpretation
- in
- let term' = parser_mk_term filled_interpretation in
- refine metasenv context term'
- in
- (* (4) build all possible interpretations *)
- let rec aux current_interpretation todo_dom =
- if Domain.is_empty todo_dom then
- match test_interpretation current_interpretation Domain.empty with
- | Ok (term, metasenv) -> [ current_interpretation, term, metasenv ]
- | Ko | Uncertain -> []
- else
- let item = Domain.choose todo_dom in
- debug_print (sprintf "CHOOSED ITEM: %s"
- (string_of_interpretation_domain_item item));
- let remaining_dom = Domain.remove item todo_dom in
- let choices = lookup_choices item in
- let rec filter = function
- | [] -> []
- | codomain_item :: tl ->
- let new_interpretation =
- fun item' ->
- if item' = item then
- codomain_item
- else
- current_interpretation item'
- in
- (match test_interpretation new_interpretation remaining_dom with
- | Ok (term, metasenv) ->
- (if Domain.is_empty remaining_dom then
- [ new_interpretation, term, metasenv ]
- else
- aux new_interpretation remaining_dom)
- @ filter tl
- | Uncertain ->
- (if Domain.is_empty remaining_dom then
- []
- else
- aux new_interpretation remaining_dom)
- @ filter tl
- | Ko -> filter tl)
- in
- filter choices
- in
- let (choosed_interpretation, choosed_term, choosed_metasenv) =
- match aux current_interpretation todo_dom with
- | [] -> raise NoWellTypedInterpretation
- | [ x ] ->
- debug_print "UNA SOLA SCELTA";
- x
- | l ->
- debug_print "PIU' SCELTE";
- let choices =
- List.map
- (fun (interpretation, _, _) ->
- List.map
- (fun domain_item ->
- let description = fst (interpretation domain_item) in
-(*
- match interpretation domain_item with
- | None -> assert false
- | Some (descr, _) -> descr
- in
-*)
- (descr_of_domain_item domain_item, description))
- (Domain.elements parser_dom))
- l
- in
- let choosed = C.interactive_interpretation_choice choices in
- List.nth l choosed
- in
- (Domain.union current_dom todo_dom, choosed_interpretation),
- choosed_metasenv, choosed_term
-
- end
+let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
+ snd (Environment.find item env) env num args
-let apply_interp (interp: interpretation) item = snd (interp item)
+let find_in_environment name context =
+ let rec aux acc = function
+ | [] -> raise Not_found
+ | Cic.Name hd :: tl when hd = name -> acc
+ | _ :: tl -> aux (acc + 1) tl
+ in
+ aux 1 context
-let interpretate ~context ~interp ast =
+let interpretate ~context ~env ast =
let rec aux loc context = function
| Ast.LocatedTerm (loc, term) -> aux loc context term
| Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
- | Ast.Appl_symbol (symb, args) ->
+ | Ast.Appl_symbol (symb, i, args) ->
let cic_args = List.map (aux loc context) args in
- apply_interp interp (Symbol (symb, 0)) interp cic_args
+ resolve env (Symbol (symb, i)) ~args:cic_args ()
| Ast.Binder (binder_kind, var, typ, body) ->
let cic_type = aux_option loc context typ in
- let cic_body = aux loc (Some var :: context) body in
+ let cic_body = aux loc (var :: context) body in
(match binder_kind with
| `Lambda -> Cic.Lambda (var, cic_type, cic_body)
| `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
| `Exists ->
- apply_interp interp (Symbol ("exists", 0)) interp
- [ cic_type; Cic.Lambda (var, cic_type, cic_body) ])
+ resolve env (Symbol ("exists", 0))
+ ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
| Ast.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux loc context term in
let cic_outtype = aux_option loc context outtype in
let rec do_branch' context = function
| [] -> aux loc context term
| hd :: tl ->
- let cic_body = do_branch' (Some (Cic.Name hd) :: context) tl in
+ let cic_body = do_branch' (Cic.Name hd :: context) tl in
Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body)
in
match pat with
| [] -> assert false
in
let (indtype_uri, indtype_no) =
- match apply_interp interp (Id indty_ident) interp [] with
+ match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> uri, tyno
+ | Cic.Implicit -> raise Try_again
| _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident)
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
| Ast.LetIn (var, def, body) ->
let cic_def = aux loc context def in
let name = Cic.Name var in
- let cic_body = aux loc (Some name :: context) body in
+ let cic_body = aux loc (name :: context) body in
Cic.LetIn (name, cic_def, cic_body)
| Ast.LetRec (kind, defs, body) ->
let context' =
- List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
+ List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
context defs
in
let cic_body = aux loc context' body in
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
| Ast.Ident (name, subst) ->
- let rec find acc e = function
- | [] -> raise Not_found
- | Some (Cic.Name hd) :: tl when e = hd -> acc
- | _ :: tl -> find (acc + 1) e tl
- in
+ (* TODO hanlde explicit substitutions *)
(try
- let index = find 1 name context in
+ let index = find_in_environment name context in
if subst <> [] then
Parser.fail loc "Explicit substitutions not allowed here";
Cic.Rel index
- with Not_found ->
- apply_interp interp (Id name) interp [])
- | Ast.Num num -> apply_interp interp (Num (num, 0)) interp []
+ with Not_found -> resolve env (Id name) ())
+ | Ast.Num (num, i) -> resolve env (Num i) ~num ()
| Ast.Meta (index, subst) ->
let cic_subst =
List.map
| Ast.LocatedTerm (loc, term) -> aux loc context term
| _ -> assert false
+let domain_of_term ~context ast =
+ let rec aux loc context = function
+ | Ast.LocatedTerm (_, term) -> aux loc context term
+ | Ast.Appl terms ->
+ List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
+ Domain.empty terms
+ | Ast.Appl_symbol (symb, i, args) ->
+ List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
+ (Domain.singleton (Symbol (symb, i))) args
+ | Ast.Binder (_, var, typ, body) ->
+ let type_dom = aux_option loc context typ in
+ let body_dom = aux loc (var :: context) body in
+ Domain.union type_dom body_dom
+ | Ast.Case (term, indty_ident, outtype, branches) ->
+ let term_dom = aux loc context term in
+ let outtype_dom = aux_option loc context outtype in
+ let do_branch (pat, term) =
+ match pat with
+ | _ :: tl ->
+ aux loc
+ (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
+ context tl)
+ term
+ | [] -> assert false
+ in
+ let branches_dom =
+ List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
+ Domain.empty branches
+ in
+ Domain.add (Id indty_ident)
+ (Domain.union outtype_dom (Domain.union term_dom branches_dom))
+ | Ast.LetIn (var, body, where) ->
+ let body_dom = aux loc context body in
+ let where_dom = aux loc (Cic.Name var :: context) where in
+ Domain.union body_dom where_dom
+ | Ast.LetRec (kind, defs, where) ->
+ let context' =
+ List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
+ context defs
+ in
+ let where_dom = aux loc context' where in
+ let defs_dom =
+ List.fold_left
+ (fun dom (_, body, typ, _) ->
+ Domain.union (aux loc context' body) (aux_option loc context typ))
+ Domain.empty defs
+ in
+ Domain.union where_dom defs_dom
+ | Ast.Ident (name, subst) ->
+ (* TODO hanlde explicit substitutions *)
+ (try
+ let index = find_in_environment name context in
+ if subst <> [] then
+ Parser.fail loc "Explicit substitutions not allowed here";
+ Domain.empty
+ with Not_found -> Domain.singleton (Id name))
+ | Ast.Num (num, i) -> Domain.singleton (Num i)
+ | Ast.Meta (index, local_context) ->
+ List.fold_left
+ (fun dom term -> Domain.union dom (aux_option loc context term))
+ Domain.empty local_context
+ | Ast.Sort _ -> Domain.empty
+ and aux_option loc context = function
+ | None -> Domain.empty
+ | Some t -> aux loc context t
+ in
+ match ast with
+ | Ast.LocatedTerm (loc, term) -> aux loc context term
+ | _ -> assert false
+
+module Make (C: Callbacks) =
+ struct
+ let choices_of_id mqi_handle id =
+ let query = MQueryGenerator.locate id in
+ let result = MQueryInterpreter.execute mqi_handle query in
+ let uris =
+ List.map
+ (function uri,_ ->
+ MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ C.output_html (`Msg (`T "Locate query:"));
+ MQueryUtil.text_of_query
+ (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+ "" query;
+ C.output_html (`Msg (`T "Result:"));
+ MQueryUtil.text_of_result
+ (fun s -> C.output_html (`Msg (`T s))) "" result;
+ let uris' =
+ match uris with
+ | [] ->
+ [UriManager.string_of_uri (C.input_or_locate_uri
+ ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ | [uri] -> [uri]
+ | _ ->
+ C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
+ ~ok:"Try every selection." ~enable_button_for_non_vars:true
+ ~title:"Ambiguous input." ~id
+ ~msg: ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one or more interpretations:")
+ uris
+ in
+ List.map
+ (fun uri -> (uri, let term = term_of_uri uri in fun _ _ _ -> term))
+ uris'
+
+ let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+ =
+ let current_dom = (* TODO temporary, remove ASAP *)
+ Environment.fold (fun item _ dom -> Domain.add item dom)
+ current_env Domain.empty
+ in
+ debug_print "NEW DISAMBIGUATE INPUT";
+ let disambiguate_context = (* cic context -> disambiguate context *)
+ List.map
+ (function None -> Cic.Anonymous | Some (name, _) -> name)
+ context
+ in
+ let term_dom = domain_of_term ~context:disambiguate_context term in
+ debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
+ (string_of_domain term_dom));
+ let todo_dom = Domain.diff term_dom current_dom in
+ (* (2) lookup function for any item (Id/Symbol/Num) *)
+ let lookup_choices =
+ let id_choices = Hashtbl.create 1023 in
+ fun item ->
+ let choices =
+ match item with
+ | Id id ->
+ (try
+ Hashtbl.find id_choices id
+ with Not_found ->
+ let choices = choices_of_id mqi_handle id in
+ Hashtbl.add id_choices id choices;
+ choices)
+ | Symbol (symb, _) ->
+ (try Hashtbl.find symbol_choices symb with Not_found -> [])
+ | Num instance -> !num_choices
+ in
+ if choices = [] then raise (No_choices item);
+ choices
+ in
+ (* (3) test an interpretation filling with meta uninterpreted identifiers
+ *)
+ let test_env current_env todo_dom =
+ let filled_env =
+ Domain.fold
+ (fun item env ->
+ Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+ todo_dom current_env
+ in
+ try
+ let cic_term =
+ interpretate ~context:disambiguate_context ~env:filled_env term
+ in
+ debug_print
+ (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm cic_term));
+ refine metasenv context cic_term
+ with
+ | Try_again -> Uncertain
+ | Invalid_choice -> Ko
+ in
+ (* (4) build all possible interpretations *)
+ let rec aux current_env todo_dom =
+ if Domain.is_empty todo_dom then
+ match test_env current_env Domain.empty with
+ | Ok (term, metasenv) -> [ current_env, term, metasenv ]
+ | Ko | Uncertain -> []
+ else
+ let item = Domain.choose todo_dom in
+ let remaining_dom = Domain.remove item todo_dom in
+ debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
+ let choices = lookup_choices item in
+ let rec filter = function
+ | [] -> []
+ | codomain_item :: tl ->
+ let new_env = Environment.add item codomain_item current_env in
+ (match test_env new_env remaining_dom with
+ | Ok (term, metasenv) ->
+ (if Domain.is_empty remaining_dom then
+ [ new_env, term, metasenv ]
+ else
+ aux new_env remaining_dom)
+ @ filter tl
+ | Uncertain ->
+ (if Domain.is_empty remaining_dom then
+ []
+ else
+ aux new_env remaining_dom)
+ @ filter tl
+ | Ko -> filter tl)
+ in
+ filter choices
+ in
+ let (choosed_env, choosed_term, choosed_metasenv) =
+ match aux current_env todo_dom with
+ | [] -> raise NoWellTypedInterpretation
+ | [ x ] ->
+ debug_print "UNA SOLA SCELTA";
+ x
+ | l ->
+ debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+ let choices =
+ List.map
+ (fun (env, _, _) ->
+ List.map
+ (fun domain_item ->
+ let description =
+ fst (Environment.find domain_item env)
+ in
+ (descr_of_domain_item domain_item, description))
+ (Domain.elements term_dom))
+ l
+ in
+ let choosed = C.interactive_interpretation_choice choices in
+ List.nth l choosed
+ in
+ (choosed_env, choosed_metasenv, choosed_term)
+
+ end
+
* http://helm.cs.unibo.it/
*)
-open Disambiguate_struct
open Disambiguate_types
-type interpretation_domain = Domain.t
-type domain_and_interpretation = interpretation_domain * interpretation
+ (* TODO move to CicSomething *)
+val term_of_uri: string -> Cic.term
-(*
-val add_symbol_choice:
- string -> string * interpretation_codomain_item -> unit
-val add_symbol_choices:
- string -> (string * interpretation_codomain_item) list -> unit
+(** {2 Choice registration interface} *)
-val add_num_choice: string * interpretation_codomain_item -> unit
-*)
+ (** to be raised when a choice is invalid due to some given parameter (e.g.
+ * wrong number of Cic.term arguments received) *)
+exception Invalid_choice
-module Make (C : Callbacks) :
- sig
- exception NoWellTypedInterpretation
-
- val disambiguate_input :
- MQIConn.handle -> Cic.context -> Cic.metasenv ->
- interpretation_domain -> (* items occuring in parser output *)
- (interpretation -> Cic.term) -> (* parser output *)
- domain_and_interpretation -> (* current interpretation status *)
- domain_and_interpretation * Cic.metasenv * Cic.term
- (* new interpretstaion status, new metasenv, disambiguated term *)
- end
+ (** register a new symbol choice *)
+val add_symbol_choice: string -> codomain_item -> unit
- (* TODO move to CicSomething *)
-val term_of_uri: string -> Cic.term
+ (** register a new number choice *)
+val add_num_choice: codomain_item -> unit
+
+(** {2 Disambiguation interface} *)
-val interpretate:
- context: Cic.name option list -> interp: interpretation -> Ast.term ->
- Cic.term
+exception NoWellTypedInterpretation
+
+module Make (C : Callbacks) :
+ sig
+ val disambiguate_term :
+ MQIConn.handle ->
+ Cic.context ->
+ Cic.metasenv ->
+ Ast.term ->
+ aliases:environment -> (* previous interpretation status *)
+ environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term (* disambiguated term *)
+ end
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-open Disambiguate_types
-
-module OrderedDomain =
- struct
- type t = interpretation_domain_item
- let compare = Pervasives.compare
- end
-
-module Domain = Set.Make(OrderedDomain)
-
-module type Callbacks =
- sig
- val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
- val interactive_user_uri_choice :
- selection_mode:[`SINGLE | `MULTIPLE] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> string list -> string list
- val interactive_interpretation_choice :
- (string * string) list list -> int
- val input_or_locate_uri : title:string -> UriManager.uri
- end
-
--- /dev/null
+
+type domain_item =
+ | Id of string (* literal *)
+ | Symbol of string * int (* literal, instance num *)
+ | Num of int (* instance num *)
+
+module OrderedDomain =
+ struct
+ type t = domain_item
+ let compare = Pervasives.compare
+ end
+
+module Domain = Set.Make (OrderedDomain)
+module Environment = Map.Make (OrderedDomain)
+
+type codomain_item =
+ string * (* description *)
+ (environment -> string -> Cic.term list -> Cic.term)
+ (* environment, literal number, arguments as needed *)
+
+and environment = codomain_item Environment.t
+
+module type Callbacks =
+ sig
+ val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> string list -> string list
+ val interactive_interpretation_choice :
+ (string * string) list list -> int
+ val input_or_locate_uri : title:string -> UriManager.uri
+ end
+
+let string_of_domain_item = function
+ | Id s -> Printf.sprintf "ID(%s)" s
+ | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
+ | Num i -> Printf.sprintf "NUM(instance %d)" i
+
+let string_of_domain dom =
+ let buf = Buffer.create 1024 in
+ Domain.iter
+ (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; "))
+ dom;
+ Buffer.contents buf
+
* http://helm.cs.unibo.it/
*)
-type interpretation_domain_item =
+type domain_item =
| Id of string (* literal *)
| Symbol of string * int (* literal, instance num *)
- | Num of string * int (* literal, instance num *)
+ | Num of int (* instance num *)
-and interpretation_codomain_item =
+module Domain: Set.S with type elt = domain_item
+module Environment: Map.S with type key = domain_item
+
+type codomain_item =
string * (* description *)
- (interpretation -> Cic.term list -> Cic.term)
+ (environment -> string -> Cic.term list -> Cic.term)
+ (* environment, literal number, arguments as needed *)
+
+and environment = codomain_item Environment.t
+
+module type Callbacks =
+ sig
+ val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> string list -> string list
+ val interactive_interpretation_choice :
+ (string * string) list list -> int
+ val input_or_locate_uri : title:string -> UriManager.uri
+ end
-and interpretation = interpretation_domain_item -> interpretation_codomain_item
+val string_of_domain_item: domain_item -> string
+val string_of_domain: Domain.t -> string
exception Error of int * int * string
+exception Not_an_extended_ident
+
let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ]
let regexp digit = [ '0' - '9' ]
let regexp blank = [ ' ' '\t' '\n' ]
let regexp blanks = blank+
let regexp num = digit+
-let regexp ident = alpha (alpha | num)*
-let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ]
let regexp tex_token = '\\' alpha+
+let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ]
+let regexp ident_cont = alpha | num | '_'
+let regexp ident_cont' = ident_cont | tex_token
+let regexp ident = (alpha ident_cont*) | ('_' ident_cont+)
+let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+)
let regexp lparen = [ '(' '[' '{' ]
let regexp rparen = [ ')' ']' '}' ]
let regexp meta = '?' num
+(* let regexp catchall = .* *)
let keywords = Hashtbl.create 17
let _ =
let return lexbuf token = (token, Ulexing.loc lexbuf)
+(*
+let parse_ext_ident ident =
+ let len = String.length ident in
+ let buf = Buffer.create len in
+ let in_tex_token = ref false in
+ let tex_token = Buffer.create 10 in
+ try
+ for i = 0 to len - 1 do
+ match ident.[i] with
+ | '\' when not !in_tex_token ->
+ if i < len - 1 &&
+ in_tex_token := true
+ done
+ with Invalid_argument -> assert false
+
+let rec token' = lexer
+ | ident' ->
+ (try
+ let ident = parse_ext_ident (Ulexing.utf8_lexeme lexbuf) in
+ return lexbuf ("IDENT'", ident)
+ with Not_an_extended_ident ->
+ Ulexing.rollback lexbuf;
+ token lexbuf)
+ | _ ->
+ Ulexing.rollback lexbuf;
+ token lexbuf
+
+and token = lexer
+*)
let rec token = lexer
-| blanks -> token lexbuf
-| ident ->
- let lexeme = Ulexing.utf8_lexeme lexbuf in
- (try
- return lexbuf (Hashtbl.find keywords lexeme)
- with Not_found ->
- return lexbuf ("IDENT", lexeme))
-| num -> return lexbuf ("INT", Ulexing.utf8_lexeme lexbuf)
-| lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf)
-| rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf)
-| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
-| symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
-| tex_token ->
- let macro =
- Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
- in
- (try
- return lexbuf ("SYMBOL", Macro.expand macro)
- with Macro.Macro_not_found _ ->
- return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf))
-| eof -> return lexbuf ("EOI", "")
-| _ -> error lexbuf "Invalid character"
+ | blanks -> token lexbuf
+ | ident ->
+ let lexeme = Ulexing.utf8_lexeme lexbuf in
+ (try
+ return lexbuf (Hashtbl.find keywords lexeme)
+ with Not_found -> return lexbuf ("IDENT", lexeme))
+ | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf)
+ | lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf)
+ | rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf)
+ | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
+ | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
+ | tex_token ->
+ let macro =
+ Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
+ in
+ (try
+ return lexbuf ("SYMBOL", Macro.expand macro)
+ with Macro.Macro_not_found _ ->
+ return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf))
+ | eof -> return lexbuf ("EOI", "")
+ | _ -> error lexbuf "Invalid character"
let tok_func stream =
let lexbuf = Ulexing.from_utf8_stream stream in
EXTEND
term: LEVEL "add"
[
- [ t1 = term; SYMBOL "∨"; t2 = term ->
- return_term loc (Appl_symbol ("or", [t1; t2]))
+ [ t1 = term; SYMBOL <:unicode<lor>> (* ∨ *); t2 = term ->
+ return_term loc (Appl_symbol ("or", 0, [t1; t2]))
]
];
term: LEVEL "mult"
[
- [ t1 = term; SYMBOL "∧"; t2 = term ->
- return_term loc (Appl_symbol ("and", [t1; t2]))
+ [ t1 = term; SYMBOL <:unicode<land>> (* ∧ *); t2 = term ->
+ return_term loc (Appl_symbol ("and", 0, [t1; t2]))
]
];
term: LEVEL "inv"
[
- [ SYMBOL "¬"; t = term -> return_term loc (Appl_symbol ("not", [t])) ]
+ [ SYMBOL <:unicode<lnot>> (* ¬ *); t = term ->
+ return_term loc (Appl_symbol ("not", 0, [t])) ]
];
END
+
+let _ =
+ Disambiguate.add_symbol_choice "eq"
+ ("leibnitz's equality",
+ (fun interp _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise Disambiguate.Invalid_choice
+ in
+ Cic.Appl [
+ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ Cic.Implicit; t1; t2
+ ]))
+
*)
let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline s
let loc = (0, 0)
]
| "eq" LEFTA
[ t1 = term; SYMBOL "="; t2 = term ->
- return_term loc (Ast.Appl_symbol ("eq", [t1; t2]))
+ return_term loc (Ast.Appl_symbol ("eq", 0, [t1; t2]))
]
| "add" LEFTA [ (* nothing here by default *) ]
| "mult" LEFTA [ (* nothing here by default *) ]
| "inv" NONA [ (* nothing here by default *) ]
| "simple" NONA
[
+ (* TODO handle "_" *)
b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ];
SYMBOL "."; body = term ->
| n = substituted_name -> return_term loc n
| LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
return_term loc (Ast.Appl (head :: args))
- | i = INT -> return_term loc (Ast.Num i)
+ | i = NUM -> return_term loc (Ast.Num (i, 0))
+(* | i = NUM -> return_term loc (Ast.Num (i, Random.int max_int)) *)
| m = META;
substs = [
LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
let parse_term = Grammar.Entry.parse term
-(*
-open Disambiguate_struct
-open ProofEngineHelpers
-
-exception UnknownIdentifier of string
-exception InductiveTypeExpected
-
-let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom []
-let apply_interp (interp: interpretation) item = snd (interp item)
-
-let pre_disambiguate ~context ast =
- let rec aux loc context = function
- | Ast.LocatedTerm (loc, term) -> aux loc context term
- | Ast.Appl terms ->
- let (dom, funs) =
- List.fold_left
- (fun (dom, funs) term ->
- let (dom', f) = aux loc context term in
- (Domain.union dom dom', f :: funs))
- (Domain.empty, [])
- terms
- in
- let f interp =
- Cic.Appl (List.map (fun f -> f interp) (List.rev funs))
- in
- (dom, f)
- | Ast.Appl_symbol (symb, args) ->
- let (dom, funs) =
- List.fold_left
- (fun (dom, funs) term ->
- let (dom', f) = aux loc context term in
- (Domain.union dom dom', f :: funs))
- (Domain.empty, [])
- args
- in
- (Domain.add (Symbol (symb, 0)) dom,
- (fun interp ->
- apply_interp interp (Symbol (symb, 0)) interp
- (List.map (fun f -> f interp) funs)))
- | Ast.Binder (binder_kind, var, typ, body) ->
- let (type_dom, type_f) =
- match typ with
- | Some t -> aux loc context t
- | None -> (Domain.empty, (fun _ -> Cic.Implicit))
- in
- let (dom', body_f) = aux loc (Some var :: context) body in
- let dom'' = Domain.union dom' type_dom in
- (dom'',
- match binder_kind with
- | `Lambda ->
- (fun interp ->
- Cic.Lambda (var, type_f interp, body_f interp))
- | `Pi | `Forall ->
- (fun interp ->
- Cic.Prod (var, type_f interp, body_f interp))
- | `Exists ->
- (fun interp ->
- let typ = type_f interp in
- Cic.Appl
- [ apply_interp interp (Id "ex") interp [];
- typ;
- (Cic.Lambda (var, typ, body_f interp)) ]))
- | Ast.Case (term, indty_ident, outtype, branches) ->
- let (term_dom, term_f) = aux loc context term in
- let (outtype_dom, outtype_f) =
- match outtype with
- | Some typ -> aux loc context typ
- | None -> (Domain.empty, (fun _ -> Cic.Implicit))
- in
- let do_branch (pat, term) =
- let rec do_branch' context = function
- | [] -> aux loc context term
- | hd :: tl ->
- let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in
- (dom,
- (fun interp ->
- Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp)))
- in
- match pat with
- | _ :: tl -> (* ignoring constructor *)
- do_branch' context tl
- | [] -> assert false
- in
- let (branches_dom, branches_f) =
- List.fold_right
- (fun branch (dom, f) ->
- let (dom', f') = do_branch branch in
- Domain.union dom dom', (fun interp -> f' interp :: f interp))
- branches
- (Domain.empty, (fun _ -> []))
- in
- (Domain.union outtype_dom (Domain.union term_dom branches_dom),
- (fun interp ->
- let (indtype_uri, indtype_no) =
- match apply_interp interp (Id indty_ident) interp [] with
- | Cic.MutInd (uri, tyno, _) -> uri, tyno
- | _ -> assert false
- in
- Cic.MutCase (indtype_uri, indtype_no, outtype_f interp,
- term_f interp, branches_f interp)))
- | Ast.LetIn (var, body, where) ->
- let (body_dom, body_f) = aux loc context body in
- let (where_dom, where_f) = aux loc context where in
- (Domain.union body_dom where_dom,
- fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp))
- | Ast.LetRec (kind, defs, where) ->
- let context' =
- List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
- context defs
- in
- let (where_dom, where_f) = aux loc context' where in
- let inductiveFuns =
- List.map
- (fun (var, body, typ, decr_idx) ->
- let body_dom, body_f = aux loc context' body in
- let typ_dom, typ_f =
- match typ with
- | None -> (Domain.empty, (fun _ -> Cic.Implicit))
- | Some typ -> aux loc context' typ
- in
- (Domain.union body_dom typ_dom,
- (fun interp ->
- (var, decr_idx, typ_f interp, body_f interp))))
- defs
- in
- let dom =
- List.fold_left (fun acc (dom, _) -> Domain.union acc dom)
- where_dom inductiveFuns
- in
- let inductiveFuns interp =
- List.map (fun (_, g) -> g interp) inductiveFuns
- in
- let build_term counter funs =
- (* this is the body of the fold_right function below. Rationale: Fix
- * and CoFix cases differs only in an additional index in the
- * indcutiveFun list, see Cic.term *)
- match kind with
- | `Inductive ->
- (fun (var, _, _, _) cic ->
- incr counter;
- Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
- | `CoInductive ->
- let funs =
- List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
- in
- (fun (var, _, _, _) cic ->
- Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
- in
- (dom,
- (fun interp ->
- let counter = ref 0 in
- let funs = inductiveFuns interp in
- List.fold_right (build_term counter funs) funs (where_f interp)))
- | Ast.Ident (name, subst) ->
- (* TODO hanlde explicit substitutions *)
- let rec find acc e = function
- | [] -> raise Not_found
- | Some (Cic.Name hd) :: tl when e = hd -> acc
- | _ :: tl -> find (acc + 1) e tl
- in
- (try
- let index = find 1 name context in
- if subst <> [] then
- fail loc "Explicit substitutions not allowed here";
- (Domain.empty, fun _ -> Cic.Rel index)
- with Not_found ->
- (Domain.singleton (Id name),
- (fun interp -> apply_interp interp (Id name) interp [])))
- | Ast.Num num ->
- (* TODO check to see if num can be removed from the domain *)
- (Domain.singleton (Num (num, 0)),
- (fun interp -> apply_interp interp (Num (num, 0)) interp []))
- | Ast.Meta (index, subst) ->
- let (dom, funs) =
- List.fold_left
- (fun (dom, funs) term ->
- match term with
- | None -> (dom, (fun _ -> None) :: funs)
- | Some term ->
- let (dom', f) = aux loc context term in
- (Domain.union dom dom',
- (fun interp -> Some (f interp)) :: funs))
- (Domain.empty, [])
- subst
- in
- let f interp =
- Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs))
- in
- (dom, f)
- | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop
- | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set
- | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type
- | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp
- in
- match ast with
- | Ast.LocatedTerm (loc, term) ->
- let (dom, f) = aux loc context term in
- dom, f
- | _ -> assert false
-
-let main ~context char_stream =
- let term_ast = parse_term char_stream in
- debug_print (Pp.pp_term term_ast);
- pre_disambiguate ~context term_ast
-*)
-
(** raise a parse error *)
val fail: Ast.location -> string -> 'a
-(*
-open Disambiguate_types
-
-val main:
- context:Cic.name option list -> char Stream.t ->
- Domain.t * (interpretation -> Cic.term)
-*)
-
pp_term term
| Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms))
- | Appl_symbol (symbol, terms) ->
+ | Appl_symbol (symbol, _, terms) ->
sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms))
| Binder (kind, var, typ, body) ->
sprintf "\\%s %s%s.%s" (pp_binder kind)
sprintf "%d[%s]" index
(String.concat "; "
(List.map (function None -> "_" | Some term -> pp_term term) substs))
- | Num num -> num
+ | Num (num, _) -> num
| Sort `Set -> "Set"
| Sort `Prop -> "Prop"
| Sort `Type -> "Type"
* http://helm.cs.unibo.it/
*)
-let ic = open_in Sys.argv.(1) in
+let ic =
+ try
+ open_in Sys.argv.(1)
+ with Invalid_argument _ -> stdin
+in
let token_stream = fst (Lexer.lex.Token.tok_func (Stream.of_channel ic)) in
let rec dump () =
let (a,b) = Stream.next token_stream in
*)
try
- let ic = open_in Sys.argv.(1) in
+ let ic =
+ (try
+ open_in Sys.argv.(1)
+ with Invalid_argument _ -> stdin)
+ in
let term = Parser.parse_term (Stream.of_channel ic) in
close_in ic;
print_endline (Pp.pp_term term)
--- /dev/null
+[nat]
+match true:bool with
+[ true \Rightarrow O
+| false \Rightarrow (S O)
+]
+
+[nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x))
+]
+
+[nat]
+match nil:list with
+[ nil \Rightarrow nil
+| (cons x y) \Rightarrow (cons x y)
+]
+
projects / helm.git / commitdiff