and token = lexer
*)
+
+let remove_quotes s = String.sub s 1 (String.length s - 2)
+
let rec token comments = lexer
| blanks -> token comments lexbuf
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
| implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
| qstring ->
- let lexeme = Ulexing.utf8_lexeme lexbuf in
- let s = String.sub lexeme 1 (String.length lexeme - 2) in
- return lexbuf ("QSTRING", s)
+ return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
| symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
| tex_token ->
let macro =
let tactical = Grammar.Entry.create grammar "tactical"
let tactical0 = Grammar.Entry.create grammar "tactical0"
let command = Grammar.Entry.create grammar "command"
+let alias_spec = Grammar.Entry.create grammar "alias_spec"
+let macro = Grammar.Entry.create grammar "macro"
let script = Grammar.Entry.create grammar "script"
+let statement = Grammar.Entry.create grammar "statement"
let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
-let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
-let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
-let return_command loc cmd = cmd (* TODO ZACK FIXME uhm ... why we drop loc? *)
let fail floc msg =
let (x, y) = CicAst.loc_of_floc floc in
| None -> None
| Some lexeme -> Some (int_of_string lexeme)
+let int_of_string s =
+ try
+ Pervasives.int_of_string s
+ with Failure _ ->
+ failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
+
(** the uri of an inductive type (a ".ind" uri) is not meaningful without an
* xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind"
* actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive
vars body
EXTEND
- GLOBAL: term term0 tactic tactical tactical0 command script;
+ GLOBAL: term term0 statement;
int: [
[ num = NUM ->
try
[ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
];
reduction_kind: [
- [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
- | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
- | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
+ [ [ IDENT "reduce" ] -> `Reduce
+ | [ IDENT "simplify" ] -> `Simpl
+ | [ IDENT "whd" ] -> `Whd ]
];
tactic: [
- [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
- return_tactic loc (TacticAst.Absurd t)
- | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
- return_tactic loc (TacticAst.Apply t)
- | [ IDENT "assumption" | IDENT "Assumption" ] ->
- return_tactic loc TacticAst.Assumption
- | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
- | [ IDENT "change" | IDENT "Change" ];
+ [ [ IDENT "absurd" ]; t = tactic_term ->
+ TacticAst.Absurd (loc, t)
+ | [ IDENT "apply" ]; t = tactic_term ->
+ TacticAst.Apply (loc, t)
+ | [ IDENT "assumption" ] ->
+ TacticAst.Assumption loc
+ | [ IDENT "auto" ] -> TacticAst.Auto loc
+ | [ IDENT "change" ];
t1 = tactic_term; "with"; t2 = tactic_term;
where = tactic_where ->
- return_tactic loc (TacticAst.Change (t1, t2, where))
+ TacticAst.Change (loc, t1, t2, where)
(* TODO Change_pattern *)
- | [ IDENT "contradiction" | IDENT "Contradiction" ] ->
- return_tactic loc TacticAst.Contradiction
- | [ IDENT "cut" | IDENT "Cut" ];
- t = tactic_term -> return_tactic loc (TacticAst.Cut t)
- | [ IDENT "decompose" | IDENT "Decompose" ];
+ | [ IDENT "contradiction" ] ->
+ TacticAst.Contradiction loc
+ | [ IDENT "cut" ];
+ t = tactic_term ->
+ TacticAst.Cut (loc, t)
+ | [ IDENT "decompose" ];
principles = ident_list1; where = IDENT ->
- return_tactic loc (TacticAst.Decompose (where, principles))
- | [ IDENT "discriminate" | IDENT "Discriminate" ];
+ TacticAst.Decompose (loc, where, principles)
+ | [ IDENT "discriminate" ];
hyp = IDENT ->
- return_tactic loc (TacticAst.Discriminate hyp)
- | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
- return_tactic loc (TacticAst.ElimType t)
- | [ IDENT "elim" | IDENT "Elim" ];
+ TacticAst.Discriminate (loc, hyp)
+ | [ IDENT "elimType" ]; t = tactic_term ->
+ TacticAst.ElimType (loc, t)
+ | [ IDENT "elim" ];
t1 = tactic_term;
using = OPT [ "using"; using = tactic_term -> using ] ->
- return_tactic loc (TacticAst.Elim (t1, using))
- | [ IDENT "exact" | IDENT "Exact" ]; t = tactic_term ->
- return_tactic loc (TacticAst.Exact t)
- | [ IDENT "exists" | IDENT "Exists" ] ->
- return_tactic loc TacticAst.Exists
- | [ IDENT "fold" | IDENT "Fold" ];
+ TacticAst.Elim (loc, t1, using)
+ | [ IDENT "exact" ]; t = tactic_term ->
+ TacticAst.Exact (loc, t)
+ | [ IDENT "exists" ] ->
+ TacticAst.Exists loc
+ | [ IDENT "fold" ];
kind = reduction_kind; t = tactic_term ->
- return_tactic loc (TacticAst.Fold (kind, t))
- | [ IDENT "fourier" | IDENT "Fourier" ] ->
- return_tactic loc TacticAst.Fourier
- | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint
- | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
- return_tactic loc (TacticAst.Injection ident)
- | [ IDENT "intros" | IDENT "Intros" ];
+ TacticAst.Fold (loc, kind, t)
+ | [ IDENT "fourier" ] ->
+ TacticAst.Fourier loc
+ | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
+ | [ IDENT "hint" ] -> TacticAst.Hint loc
+ | [ IDENT "injection" ]; ident = IDENT ->
+ TacticAst.Injection (loc, ident)
+ | [ IDENT "intros" ];
num = OPT [ num = int -> num ];
idents = OPT ident_list0 ->
let idents = match idents with None -> [] | Some idents -> idents in
- return_tactic loc (TacticAst.Intros (num, idents))
- | [ IDENT "intro" | IDENT "Intro" ] ->
- return_tactic loc (TacticAst.Intros (None, []))
- | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
+ TacticAst.Intros (loc, num, idents)
+ | [ IDENT "intro" ] ->
+ TacticAst.Intros (loc, None, [])
+ | [ IDENT "left" ] -> TacticAst.Left loc
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->
- return_tactic loc (TacticAst.LetIn (t, where))
+ TacticAst.LetIn (loc, t, where)
| kind = reduction_kind;
pat = OPT [
"in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
pat
];
terms = LIST0 term SEP SYMBOL "," ->
- let tac =
- (match (pat, terms) with
- | None, [] -> TacticAst.Reduce (kind, None)
- | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
- | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
- in
- return_tactic loc tac
- | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
- return_tactic loc TacticAst.Reflexivity
- | [ IDENT "replace" | IDENT "Replace" ];
+ (match (pat, terms) with
+ | None, [] -> TacticAst.Reduce (loc, kind, None)
+ | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
+ | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+ | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ | [ IDENT "reflexivity" ] ->
+ TacticAst.Reflexivity loc
+ | [ IDENT "replace" ];
t1 = tactic_term; "with"; t2 = tactic_term ->
- return_tactic loc (TacticAst.Replace (t1, t2))
+ TacticAst.Replace (loc, t1, t2)
(* TODO Rewrite *)
(* TODO Replace_pattern *)
- | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right
- | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring
- | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split
- | [ IDENT "symmetry" | IDENT "Symmetry" ] ->
- return_tactic loc TacticAst.Symmetry
- | [ IDENT "transitivity" | IDENT "Transitivity" ];
+ | [ IDENT "right" ] -> TacticAst.Right loc
+ | [ IDENT "ring" ] -> TacticAst.Ring loc
+ | [ IDENT "split" ] -> TacticAst.Split loc
+ | [ IDENT "symmetry" ] ->
+ TacticAst.Symmetry loc
+ | [ IDENT "transitivity" ];
t = tactic_term ->
- return_tactic loc (TacticAst.Transitivity t)
+ TacticAst.Transitivity (loc, t)
]
];
- tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ];
tactical:
- [ "command" NONA
- [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
- | "sequence" LEFTA
- [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
- (match tactics with
- | [tactic] -> tactic
- | _ -> return_tactical loc (TacticAst.Seq tactics))
+ [ "sequence" LEFTA
+ [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
+ TacticAst.Seq (loc, tacticals)
]
| "then" NONA
[ tac = tactical;
PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Then (tac, tacs))
+ (TacticAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical ->
- return_tactical loc (TacticAst.Do (count, tac))
- | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical ->
- return_tactical loc (TacticAst.Repeat tac)
+ [ [ IDENT "do" ]; count = int; tac = tactical ->
+ TacticAst.Do (loc, count, tac)
+ | [ IDENT "repeat" ]; tac = tactical ->
+ TacticAst.Repeat (loc, tac)
]
| "simple" NONA
- [ [ IDENT "tries" | IDENT "Tries" ];
+ [ IDENT "tries";
PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Tries tacs)
- | [ IDENT "try" | IDENT "Try" ]; tac = NEXT ->
- return_tactical loc (TacticAst.Try tac)
- | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail
- | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
- | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
- | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+ TacticAst.Tries (loc, tacs)
+ | IDENT "try"; tac = NEXT ->
+ TacticAst.Try (loc, tac)
+ | IDENT "fail" -> TacticAst.Fail loc
+ | IDENT "id" -> TacticAst.IdTac loc
+ | PAREN "("; tac = tactical; PAREN ")" -> tac
+ | tac = tactic -> TacticAst.Tactic (loc, tac)
]
];
- theorem_flavour: [ (* all flavours but Goal *)
- [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition
- | [ IDENT "fact" | IDENT "Fact" ] -> `Fact
- | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma
- | [ IDENT "remark" | IDENT "Remark" ] -> `Remark
- | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem
+ theorem_flavour: [
+ [ [ IDENT "definition" ] -> `Definition
+ | [ IDENT "fact" ] -> `Fact
+ | [ IDENT "lemma" ] -> `Lemma
+ | [ IDENT "remark" ] -> `Remark
+ | [ IDENT "theorem" ] -> `Theorem
]
];
inductive_spec: [ [
let ind_types = fst_ind_type :: tl_ind_types in
(params, ind_types)
] ];
- print_kind: [
- [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
- -> `Env
- | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
- -> `Coer
- ] ];
- command: [
- [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
- | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
- | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
- | [ IDENT "qed" | IDENT "Qed" ] ->
- return_command loc (TacticAst.Qed None)
- | [ IDENT "print" | IDENT "Print" ];
- print_kind = print_kind ->
- return_command loc (TacticAst.Print print_kind)
- | [ IDENT "save" | IDENT "Save" ]; name = IDENT ->
- return_command loc (TacticAst.Qed (Some name))
+ macro: [[
+ [ IDENT "abort" ] -> TacticAst.Abort loc
+ | [ IDENT "quit" ] -> TacticAst.Quit loc
+ | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+ | [ IDENT "undo" ]; steps = OPT NUM ->
+ TacticAst.Undo (loc, int_opt steps)
+ | [ IDENT "redo" ]; steps = OPT NUM ->
+ TacticAst.Redo (loc, int_opt steps)
+ | [ IDENT "check" ]; t = term ->
+ TacticAst.Check (loc, t)
+ | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+ ]];
+
+ alias_spec: [
+ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
+ let alpha = "[a-zA-Z]" in
+ let num = "[0-9]+" in
+ let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
+ let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+ let rex = Str.regexp ("^"^ident^"$") in
+ if Str.string_match rex id 0 then
+ let rex = Str.regexp
+ ("^\\(cic:/\\|theory:/\\)"^ident^
+ "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
+ "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$")
+ in
+ if Str.string_match rex uri 0 then
+ TacticAst.Ident_alias (id, uri)
+ else
+ raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))
+ else
+ raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id))
+ | IDENT "symbol"; symbol = QSTRING;
+ instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> int_of_string i | None -> 0
+ in
+ TacticAst.Symbol_alias (symbol, instance, dsc)
+ | IDENT "num";
+ instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> int_of_string i | None -> 0
+ in
+ TacticAst.Number_alias (instance, dsc)
+ ]
+ ];
+
+ command: [[
+ [ IDENT "set" ]; n = QSTRING; v = QSTRING ->
+ TacticAst.Set (loc, n, v)
+ | [ IDENT "qed" ] -> TacticAst.Qed loc
| flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+ TacticAst.Theorem (loc, flavour, name, typ, body)
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = let_defs ->
let name,ty =
| _ -> assert false
in
let body = CicAst.Ident (name,None) in
- TacticAst.Theorem(`Definition, Some name, ty,
+ TacticAst.Theorem(loc, `Definition, Some name, ty,
Some (CicAst.LetRec (ind_kind, defs, body)))
- | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
+ | [ IDENT "inductive" ]; spec = inductive_spec ->
let (params, ind_types) = spec in
- return_command loc (TacticAst.Inductive (params, ind_types))
- | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec ->
+ TacticAst.Inductive (loc, params, ind_types)
+ | [ IDENT "coinductive" ]; spec = inductive_spec ->
let (params, ind_types) = spec in
let ind_types = (* set inductive flags to false (coinductive) *)
List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
ind_types
in
- return_command loc (TacticAst.Inductive (params, ind_types))
- | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT ->
- return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some [])))
- | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI ->
- return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some [])))
- | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
- body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
- | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM ->
- return_command loc (TacticAst.Undo (int_opt steps))
- | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
- return_command loc (TacticAst.Redo (int_opt steps))
- | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
- return_command loc (TacticAst.Baseuri uri)
- | [ IDENT "basedir" | IDENT "Basedir" ]; uri = OPT QSTRING ->
- return_command loc (TacticAst.Basedir uri)
- | [ IDENT "check" | IDENT "Check" ]; t = term ->
- return_command loc (TacticAst.Check t)
-(*
- | [ IDENT "alias" | IDENT "Alias" ]; spec = alias_spec ->
- return_command loc (TacticAst.Alias spec)
-*)
- ]
- ];
- script_entry: [
- [ cmd = tactical0 -> Command cmd
-(* | s = COMMENT -> Comment (loc, s) *)
+ TacticAst.Inductive (loc, params, ind_types)
+ | [ IDENT "coercion" ] ; name = IDENT ->
+ TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
+ | [ IDENT "coercion" ] ; name = URI ->
+ TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
+ | [ IDENT "alias" ]; spec = alias_spec ->
+ TacticAst.Alias (loc, spec)
+ ]];
+
+ statement: [
+ [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
+ | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
+ | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
]
];
- script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ];
END
let exc_located_wrapper f =
let parse_term stream =
exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
-let parse_tactic stream =
- exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream))
-let parse_tactical stream =
- exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream))
-let parse_script stream =
- exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream))
+let parse_statement stream =
+ exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
(**/**)
(fun domain_item (dsc, _) acc ->
let s =
match domain_item with
- | Id id -> sprintf "alias id %s = %s" id dsc
- | Symbol (symb, instance) ->
- sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
- symb instance dsc
- | Num instance ->
- sprintf "alias num (instance %d) = \"%s\"" instance dsc
+ | Id id ->
+ TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "."
+ | Symbol (symb, i) ->
+ TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc))
+ ^ "."
+ | Num i ->
+ TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "."
in
s :: acc)
env []
(** {2 Parsing functions} *)
-val parse_term: char Stream.t -> DisambiguateTypes.term
-val parse_tactic: char Stream.t -> DisambiguateTypes.tactic
-val parse_tactical: char Stream.t -> DisambiguateTypes.tactical
-val parse_script: char Stream.t -> DisambiguateTypes.script
+val parse_term: char Stream.t -> DisambiguateTypes.term
+val parse_statement: char Stream.t -> (CicAst.term, string) TacticAst.statement
(** {2 Grammar extensions} *)
in
List.filter (fun elt -> not (is_in_dom2 elt)) dom1
+module type Disambiguator =
+sig
+ val disambiguate_term :
+ dbd:Mysql.dbd ->
+ context:Cic.context ->
+ metasenv:Cic.metasenv ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ aliases:environment -> (* previous interpretation status *)
+ CicAst.term ->
+ (environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term*
+ CicUniv.universe_graph) list (* disambiguated term *)
+end
+
module Make (C: Callbacks) =
struct
let choices_of_id dbd id =
fun _ _ _ -> term))
uris
- let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
+ let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ term
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
?(aliases=DisambiguateTypes.Environment.empty) term =
let ast = CicTextualParser2.parse_term (Stream.of_string term) in
try
- Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph
- ~aliases
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+ ?initial_ugraph ~aliases
with Exit -> raise (Ambiguous_term term)
end
exception NoWellTypedInterpretation
-module Make (C : Callbacks) :
- sig
- val disambiguate_term :
- dbd:Mysql.dbd ->
- Cic.context ->
- Cic.metasenv ->
- CicAst.term ->
- ?initial_ugraph:CicUniv.universe_graph ->
- aliases:environment -> (* previous interpretation status *)
- (environment * (* new interpretation status *)
- Cic.metasenv * (* new metasenv *)
- Cic.term*
- CicUniv.universe_graph) list (* disambiguated term *)
- end
+module type Disambiguator =
+sig
+ val disambiguate_term :
+ dbd:Mysql.dbd ->
+ context:Cic.context ->
+ metasenv:Cic.metasenv ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ aliases:environment -> (* previous interpretation status *)
+ CicAst.term ->
+ (environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term*
+ CicUniv.universe_graph) list (* disambiguated term *)
+end
+
+module Make (C : Callbacks) : Disambiguator
module Trivial:
sig
let mode =
try
match Sys.argv.(1) with
- | "alias" -> prerr_endline "Alias"; `Alias
| "term" -> prerr_endline "Term"; `Term
- | "tactic" -> prerr_endline "Tactic"; `Tactic
- | "tactical" | "command" -> prerr_endline "Tactical"; `Tactical
- | "script" -> prerr_endline "Script"; `Script
+ | "statement" -> prerr_endline "Statement"; `Statement
+(* | "script" -> prerr_endline "Script"; `Script *)
| _ ->
prerr_endline "What???????";
exit 1
with Invalid_argument _ -> prerr_endline "Term"; `Term
let _ =
+(*
if mode = `Script then
let ic = open_in Sys.argv.(2) in
let istream = Stream.of_channel ic in
| DisambiguateTypes.Comment (loc, s) -> print_endline s)
script
else
+*)
let ic = stdin in
try
while true do
| `Term ->
let term = CicTextualParser2.parse_term istream in
print_endline (BoxPp.pp_term term)
- | `Tactic ->
- let tac = CicTextualParser2.parse_tactic istream in
- print_endline (TacticAstPp.pp_tactic tac)
+ | `Statement ->
+ (match CicTextualParser2.parse_statement istream with
+ | TacticAst.Command (_, cmd) ->
+ print_endline (TacticAstPp.pp_command cmd)
+ | TacticAst.Tactical (_, tac) ->
+ print_endline (TacticAstPp.pp_tactical tac))
+(*
| `Tactical ->
let tac = CicTextualParser2.parse_tactical istream in
print_endline (pp_tactical tac)
+*)
| `Alias ->
let env = CicTextualParser2.EnvironmentP3.of_string line in
print_endline (CicTextualParser2.EnvironmentP3.to_string env)
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (_,C.Def (_,Some _)))::_ -> assert false
in
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
(* Checks suppressed *)
- CicSubstitution.lift_meta l ty
+ CicSubstitution.subst_meta l ty
| C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
C.Sort (C.Type (CicUniv.fresh()))
| C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
cicLogger.cmo: cicLogger.cmi
cicLogger.cmx: cicLogger.cmi
-cicEnvironment.cmo: cicLogger.cmi cicEnvironment.cmi
-cicEnvironment.cmx: cicLogger.cmx cicEnvironment.cmi
-cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi
-cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi
+cicEnvironment.cmo: cicEnvironment.cmi
+cicEnvironment.cmx: cicEnvironment.cmi
cicPp.cmo: cicEnvironment.cmi cicPp.cmi
cicPp.cmx: cicEnvironment.cmx cicPp.cmi
+cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi
+cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi
cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi
cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi
cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi
cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi
-cicReductionNaif.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \
- cicReductionNaif.cmi
-cicReductionNaif.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \
- cicReductionNaif.cmi
cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \
cicReduction.cmi
cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \
cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi
cicTypeChecker.cmx: cicSubstitution.cmx cicReduction.cmx cicPp.cmx \
cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi
-cicElim.cmo: cicSubstitution.cmi cicEnvironment.cmi cicElim.cmi
-cicElim.cmx: cicSubstitution.cmx cicEnvironment.cmx cicElim.cmi
+cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \
+ cicPp.cmi cicEnvironment.cmi cicElim.cmi
+cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \
+ cicPp.cmx cicEnvironment.cmx cicElim.cmi
cicUnivUtils.mli \
cicSubstitution.mli \
cicMiniReduction.mli \
- cicReductionNaif.mli \
cicReduction.mli \
cicTypeChecker.mli \
cicElim.mli
opt_utilities:
$(MAKE) -C utilities/ opt
-cicReduction.ml: $(REDUCTION_IMPLEMENTATION)
- if ! [ -f $@ ]; then \
- echo "Using $< for $@"; \
- ln -s $< $@; \
- else \
- true; \
- fi
-
clean: clean_utilities
clean_utilities:
$(MAKE) -C utilities/ clean
UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
(** remove a type checked object
- * @raise Term_not_found when given term is not in the environment
+ * @raise Object_not_found when given term is not in the environment
* @raise Failure when remove_term is invoked while type checking *)
val remove_obj: UriManager.uri -> unit
--- /dev/null
+(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
+ *)
+
+(* TODO unify exceptions *)
+
+exception CicReductionInternalError;;
+exception WrongUriToInductiveDefinition;;
+exception Impossible of int;;
+exception ReferenceToConstant;;
+exception ReferenceToVariable;;
+exception ReferenceToCurrentProof;;
+exception ReferenceToInductiveDefinition;;
+
+let fdebug = ref 1;;
+let debug t env s =
+ let rec debug_aux t i =
+ let module C = Cic in
+ let module U = UriManager in
+ CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
+ in
+ if !fdebug = 0 then
+ prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+;;
+
+module type Strategy =
+ sig
+ type stack_term
+ type env_term
+ type ens_term
+ val to_stack : Cic.term -> stack_term
+ val to_stack_list : Cic.term list -> stack_term list
+ val to_env : Cic.term -> env_term
+ val to_ens : Cic.term -> ens_term
+ val from_stack :
+ unwind:
+ (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> Cic.term) ->
+ stack_term -> Cic.term
+ val from_stack_list :
+ unwind:
+ (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> Cic.term) ->
+ stack_term list -> Cic.term list
+ val from_env : env_term -> Cic.term
+ val from_ens : ens_term -> Cic.term
+ val stack_to_env :
+ reduce:
+ (int * env_term list * ens_term Cic.explicit_named_substitution *
+ Cic.term * stack_term list -> Cic.term) ->
+ unwind:
+ (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> Cic.term) ->
+ stack_term -> env_term
+ val compute_to_env :
+ reduce:
+ (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
+ stack_term list -> Cic.term) ->
+ unwind:
+ (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> Cic.term) ->
+ int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> env_term
+ val compute_to_stack :
+ reduce:
+ (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
+ stack_term list -> Cic.term) ->
+ unwind:
+ (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> Cic.term) ->
+ int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+ Cic.term -> stack_term
+ end
+;;
+
+module CallByNameStrategy =
+ struct
+ type stack_term = Cic.term
+ type env_term = Cic.term
+ type ens_term = Cic.term
+ let to_stack v = v
+ let to_stack_list l = l
+ let to_env v = v
+ let to_ens v = v
+ let from_stack ~unwind v = v
+ let from_stack_list ~unwind l = l
+ let from_env v = v
+ let from_ens v = v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
+ let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
+ end
+;;
+
+module CallByValueStrategy =
+ struct
+ type stack_term = Cic.term
+ type env_term = Cic.term
+ type ens_term = Cic.term
+ let to_stack v = v
+ let to_stack_list l = l
+ let to_env v = v
+ let to_ens v = v
+ let from_stack ~unwind v = v
+ let from_stack_list ~unwind l = l
+ let from_env v = v
+ let from_ens v = v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
+ let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
+ end
+;;
+
+module CallByValueStrategyByNameOnConstants =
+ struct
+ type stack_term = Cic.term
+ type env_term = Cic.term
+ type ens_term = Cic.term
+ let to_stack v = v
+ let to_stack_list l = l
+ let to_env v = v
+ let to_ens v = v
+ let from_stack ~unwind v = v
+ let from_stack_list ~unwind l = l
+ let from_env v = v
+ let from_ens v = v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens =
+ function
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ let compute_to_env ~reduce ~unwind k e ens =
+ function
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ end
+;;
+
+module LazyCallByValueStrategy =
+ struct
+ type stack_term = Cic.term lazy_t
+ type env_term = Cic.term lazy_t
+ type ens_term = Cic.term lazy_t
+ let to_stack v = lazy v
+ let to_stack_list l = List.map to_stack l
+ let to_env v = lazy v
+ let to_ens v = lazy v
+ let from_stack ~unwind v = Lazy.force v
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = Lazy.force v
+ let from_ens v = Lazy.force v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
+ let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
+ end
+;;
+
+module LazyCallByValueStrategyByNameOnConstants =
+ struct
+ type stack_term = Cic.term lazy_t
+ type env_term = Cic.term lazy_t
+ type ens_term = Cic.term lazy_t
+ let to_stack v = lazy v
+ let to_stack_list l = List.map to_stack l
+ let to_env v = lazy v
+ let to_ens v = lazy v
+ let from_stack ~unwind v = Lazy.force v
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = Lazy.force v
+ let from_ens v = Lazy.force v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t =
+ lazy (
+ match t with
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[]))
+ let compute_to_env ~reduce ~unwind k e ens t =
+ lazy (
+ match t with
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[]))
+ end
+;;
+
+module LazyCallByNameStrategy =
+ struct
+ type stack_term = Cic.term lazy_t
+ type env_term = Cic.term lazy_t
+ type ens_term = Cic.term lazy_t
+ let to_stack v = lazy v
+ let to_stack_list l = List.map to_stack l
+ let to_env v = lazy v
+ let to_ens v = lazy v
+ let from_stack ~unwind v = Lazy.force v
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = Lazy.force v
+ let from_ens v = Lazy.force v
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
+ let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
+ end
+;;
+
+module
+ LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
+=
+ struct
+ type stack_term = reduce:bool -> Cic.term
+ type env_term = reduce:bool -> Cic.term
+ type ens_term = reduce:bool -> Cic.term
+ let to_stack v =
+ let value = lazy v in
+ fun ~reduce -> Lazy.force value
+ let to_stack_list l = List.map to_stack l
+ let to_env v =
+ let value = lazy v in
+ fun ~reduce -> Lazy.force value
+ let to_ens v =
+ let value = lazy v in
+ fun ~reduce -> Lazy.force value
+ let from_stack ~unwind v = (v ~reduce:false)
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = (v ~reduce:true)
+ let from_ens v = (v ~reduce:true)
+ let stack_to_env ~reduce ~unwind v = v
+ let compute_to_stack ~reduce ~unwind k e ens t =
+ let svalue =
+ lazy (
+ match t with
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ ) in
+ let lvalue =
+ lazy (unwind k e ens t)
+ in
+ fun ~reduce ->
+ if reduce then Lazy.force svalue else Lazy.force lvalue
+ let compute_to_env ~reduce ~unwind k e ens t =
+ let svalue =
+ lazy (
+ match t with
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ ) in
+ let lvalue =
+ lazy (unwind k e ens t)
+ in
+ fun ~reduce ->
+ if reduce then Lazy.force svalue else Lazy.force lvalue
+ end
+;;
+
+module ClosuresOnStackByValueFromEnvOrEnsStrategy =
+ struct
+ type stack_term =
+ int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
+ type env_term = Cic.term
+ type ens_term = Cic.term
+ let to_stack v = (0,[],[],v)
+ let to_stack_list l = List.map to_stack l
+ let to_env v = v
+ let to_ens v = v
+ let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = v
+ let from_ens v = v
+ let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
+ let compute_to_env ~reduce ~unwind k e ens t =
+ unwind k e ens t
+ let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
+ end
+;;
+
+module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
+ struct
+ type stack_term =
+ int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
+ type env_term = Cic.term
+ type ens_term = Cic.term
+ let to_stack v = (0,[],[],v)
+ let to_stack_list l = List.map to_stack l
+ let to_env v = v
+ let to_ens v = v
+ let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
+ let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+ let from_env v = v
+ let from_ens v = v
+ let stack_to_env ~reduce ~unwind (k,e,ens,t) =
+ match t with
+ Cic.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ let compute_to_env ~reduce ~unwind k e ens t =
+ unwind k e ens t
+ let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
+ end
+;;
+
+module Reduction(RS : Strategy) =
+ struct
+ type env = RS.env_term list
+ type ens = RS.ens_term Cic.explicit_named_substitution
+ type stack = RS.stack_term list
+ type config = int * env * ens * Cic.term * stack
+
+ (* k is the length of the environment e *)
+ (* m is the current depth inside the term *)
+ let unwind' m k e ens t =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ if k = 0 && ens = [] then
+ t
+ else
+ let rec unwind_aux m =
+ function
+ C.Rel n as t ->
+ if n <= m then t else
+ let d =
+ try
+ Some (RS.from_env (List.nth e (n-m-1)))
+ with _ -> None
+ in
+ (match d with
+ Some t' ->
+ if m = 0 then t' else S.lift m t'
+ | None -> C.Rel (n-k)
+ )
+ | C.Var (uri,exp_named_subst) ->
+(*
+prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+*)
+ if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
+ CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
+ else
+ let params =
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ (match o with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.Variable (_,_,_,params,_) -> params
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ in
+ let exp_named_subst' =
+ substaux_in_exp_named_subst params exp_named_subst m
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i,l) ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (unwind_aux m t)
+ ) l
+ in
+ C.Meta (i, l')
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
+ | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
+ | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
+ | C.Const (uri,exp_named_subst) ->
+ let params =
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ (match o with
+ C.Constant (_,_,_,params,_) -> params
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,_,_,params,_) -> params
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ in
+ let exp_named_subst' =
+ substaux_in_exp_named_subst params exp_named_subst m
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let params =
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ (match o with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition (_,params,_,_) -> params
+ )
+ in
+ let exp_named_subst' =
+ substaux_in_exp_named_subst params exp_named_subst m
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let params =
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ (match o with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition (_,params,_,_) -> params
+ )
+ in
+ let exp_named_subst' =
+ substaux_in_exp_named_subst params exp_named_subst m
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
+ List.map (unwind_aux m) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) ->
+ (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ and substaux_in_exp_named_subst params exp_named_subst' m =
+ (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
+ let ens' =
+ List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
+ (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
+ List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
+ in
+ let rec filter_and_lift =
+ function
+ [] -> []
+ | uri::tl ->
+ let r = filter_and_lift tl in
+ (try
+ (uri,(List.assq uri ens'))::r
+ with
+ Not_found -> r
+ )
+ in
+ filter_and_lift params
+ *)
+
+ (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
+ (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
+
+ (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
+ (*CSC: codice altamente inefficiente *)
+ let rec filter_and_lift already_instantiated =
+ function
+ [] -> []
+ | (uri,t)::tl when
+ List.for_all
+ (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
+ &&
+ not (List.mem uri already_instantiated)
+ &&
+ List.mem uri params
+ ->
+ (uri,CicSubstitution.lift m (RS.from_ens t)) ::
+ (filter_and_lift (uri::already_instantiated) tl)
+ | _::tl -> filter_and_lift already_instantiated tl
+(*
+ | (uri,_)::tl ->
+prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
+prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+if List.mem uri params then prerr_endline "---- OK2" ;
+ filter_and_lift tl
+*)
+ in
+ List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
+ (filter_and_lift [] (List.rev ens))
+ in
+ unwind_aux m t
+ ;;
+
+ let unwind =
+ unwind' 0
+ ;;
+
+ let reduce ?(subst = []) context : config -> Cic.term =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let rec reduce =
+ function
+ (k, e, _, (C.Rel n as t), s) ->
+ let d =
+ try
+ Some (RS.from_env (List.nth e (n-1)))
+ with
+ _ ->
+ try
+ begin
+ match List.nth context (n - 1 - k) with
+ None -> assert false
+ | Some (_,C.Decl _) -> None
+ | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
+ end
+ with
+ _ -> None
+ in
+ (match d with
+ Some t' -> reduce (0,[],[],t',s)
+ | None ->
+ if s = [] then
+ C.Rel (n-k)
+ else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
+ )
+ | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
+ if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
+ reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
+ else
+ ( let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ match o with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_,_,_) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else
+ C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | C.Variable (_,Some body,_,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ reduce (0, [], ens', body, s)
+ )
+ | (k, e, ens, (C.Meta (n,l) as t), s) ->
+ (try
+ let (_, term,_) = CicUtil.lookup_subst n subst in
+ reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
+ with CicUtil.Subst_not_found _ ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
+ | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
+ | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
+ | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+ reduce (k, e, ens, te, s) (* s should be empty *)
+ | (k, e, ens, (C.Prod _ as t), s) ->
+ unwind k e ens t (* s should be empty *)
+ | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
+ | (k, e, ens, C.Lambda (_,_,t), p::s) ->
+ reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
+ | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+ let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
+ reduce (k+1, m'::e, ens, t, s)
+ | (_, _, _, C.Appl [], _) -> assert false
+ | (k, e, ens, C.Appl (he::tl), s) ->
+ let tl' =
+ List.map
+ (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
+ in
+ reduce (k, e, ens, he, (List.append tl') s)
+ (* CSC: Old Dead Code
+ | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
+ (* strict evaluation, but constants are NOT unfolded *)
+ let red =
+ function
+ C.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ in
+ let tl' = List.map red tl in
+ reduce (k, e, ens, he , List.append tl' s)
+ | (k, e, ens, C.Appl l, s) ->
+ C.Appl (List.append (List.map (unwind k e ens) l) s)
+ *)
+ | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
+ (let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ match o with
+ C.Constant (_,Some body,_,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ (* constants are closed *)
+ reduce (0, [], ens', body, s)
+ | C.Constant (_,None,_,_,_) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,body,_,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ (* constants are closed *)
+ reduce (0, [], ens', body, s)
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | (k, e, ens, (C.MutInd _ as t),s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, ens, (C.MutConstruct _ as t),s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
+ let decofix =
+ function
+ C.CoFix (i,fl) as t ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ (* the term is the result of a reduction; *)
+ (* so it is already unwinded. *)
+ reduce (0,[],[],body',[])
+ | C.Appl (C.CoFix (i,fl) :: tl) ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ (* the term is the result of a reduction; *)
+ (* so it is already unwinded. *)
+ reduce (0,[],[],body',RS.to_stack_list tl)
+ | t -> t
+ in
+ (match decofix (reduce (k,e,ens,term,[])) with
+ C.MutConstruct (_,_,j,_) ->
+ reduce (k, e, ens, (List.nth pl (j-1)), s)
+ | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
+ let (arity, r) =
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
+ in
+ match o with
+ C.InductiveDefinition (tl,ingredients,r,_) ->
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
+ | _ -> raise WrongUriToInductiveDefinition
+ in
+ let ts =
+ let num_to_eat = r in
+ let rec eat_first =
+ function
+ (0,l) -> l
+ | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+ | _ -> raise (Impossible 5)
+ in
+ eat_first (num_to_eat,tl)
+ in
+ (* ts are already unwinded because they are a sublist of tl *)
+ reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
+ | C.Cast _ | C.Implicit _ ->
+ raise (Impossible 2) (* we don't trust our whd ;-) *)
+ | _ ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ )
+ | (k, e, ens, (C.Fix (i,fl) as t), s) ->
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (RS.from_stack ~unwind (List.nth s recindex))
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduce (0,[],[],recparam,[]) with
+ (* match recparam with *)
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ (* OLD
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ reduce (k, e, ens, body', s) *)
+ (* NEW *)
+ let leng = List.length fl in
+ let fl' =
+ let unwind_fl (name,recindex,typ,body) =
+ (name,recindex,unwind k e ens typ,
+ unwind' leng k e ens body)
+ in
+ List.map unwind_fl fl
+ in
+ let new_env =
+ let counter = ref 0 in
+ let rec build_env e =
+ if !counter = leng then e
+ else
+ (incr counter ;
+ build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
+ in
+ build_env e
+ in
+ reduce (k+leng, new_env, ens, body, s)
+ | _ ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else
+ C.Appl (t'::(RS.from_stack_list ~unwind s))
+ )
+ | None ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else
+ C.Appl (t'::(RS.from_stack_list ~unwind s))
+ )
+ | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ and push_exp_named_subst k e ens =
+ function
+ [] -> ens
+ | (uri,t)::tl ->
+ push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
+ in
+ reduce
+ ;;
+ (*
+ let rec whd context t =
+ try
+ reduce context (0, [], [], t, [])
+ with Not_found ->
+ prerr_endline (CicPp.ppterm t) ;
+ raise Not_found
+ ;;
+ *)
+
+ let rec whd ?(subst=[]) context t =
+ reduce ~subst context (0, [], [], t, [])
+ ;;
+
+
+(* DEBUGGING ONLY
+let whd context t =
+ let res = whd context t in
+ let rescsc = CicReductionNaif.whd context t in
+ if not (CicReductionNaif.are_convertible context res rescsc) then
+ begin
+ prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
+ flush stderr ;
+ prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
+ flush stderr ;
+ prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
+ flush stderr ;
+CicReductionNaif.fdebug := 0 ;
+let _ = CicReductionNaif.are_convertible context res rescsc in
+ assert false ;
+ end
+ else
+ res
+;;
+*)
+ end
+;;
+
+
+(*
+module R = Reduction CallByNameStrategy;;
+module R = Reduction CallByValueStrategy;;
+module R = Reduction CallByValueStrategyByNameOnConstants;;
+module R = Reduction LazyCallByValueStrategy;;
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
+module R = Reduction LazyCallByNameStrategy;;
+module R = Reduction
+ LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+module R = Reduction
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+*)
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
+
+let whd = R.whd;;
+
+ (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+ * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
+(* t1, t2 must be well-typed *)
+let are_convertible ?(subst=[]) ?(metasenv=[]) =
+ let rec aux test_equality_only context t1 t2 ugraph =
+ let aux2 test_equality_only t1 t2 ugraph =
+
+ (* this trivial euristic cuts down the total time of about five times ;-) *)
+ (* this because most of the time t1 and t2 are "sintactically" the same *)
+ if t1 === t2 then
+ true,ugraph
+ else
+ begin
+ let module C = Cic in
+ match (t1,t2) with
+ (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
+ | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
+ if U.eq uri1 uri2 then
+ (try
+ List.fold_right2
+ (fun (uri1,x) (uri2,y) (b,ugraph) ->
+ let b',ugraph' = aux test_equality_only context x y ugraph in
+ (U.eq uri1 uri2 && b' && b),ugraph'
+ ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+ with
+ Invalid_argument _ -> false,ugraph
+ )
+ else
+ false,ugraph
+ | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
+ if n1 = n2 then
+ let b2, ugraph1 =
+ let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+ let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+ List.fold_left2
+ (fun (b,ugraph) t1 t2 ->
+ if b then
+ match t1,t2 with
+ None,_
+ | _,None -> true,ugraph
+ | Some t1',Some t2' ->
+ aux test_equality_only context t1' t2' ugraph
+ else
+ false,ugraph
+ ) (true,ugraph) l1 l2
+ in
+ if b2 then true,ugraph1 else false,ugraph
+ else
+ false,ugraph
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+ true,(CicUniv.add_eq t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ true,(CicUniv.add_ge t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
+ | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+ let b',ugraph' = aux true context s1 s2 ugraph in
+ if b' then
+ aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
+ t1 t2 ugraph'
+ else
+ false,ugraph
+ | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
+ let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+ if b' then
+ aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
+ t1 t2 ugraph'
+ else
+ false,ugraph
+ | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+ let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+ if b' then
+ aux test_equality_only
+ ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
+ else
+ false,ugraph
+ | (C.Appl l1, C.Appl l2) ->
+ (try
+ List.fold_right2
+ (fun x y (b,ugraph) ->
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph) l1 l2 (true,ugraph)
+ with
+ Invalid_argument _ -> false,ugraph
+ )
+ | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
+ let b' = U.eq uri1 uri2 in
+ if b' then
+ (try
+ List.fold_right2
+ (fun (uri1,x) (uri2,y) (b,ugraph) ->
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
+ ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+ with
+ Invalid_argument _ -> false,ugraph
+ )
+ else
+ false,ugraph
+ | (C.MutInd (uri1,i1,exp_named_subst1),
+ C.MutInd (uri2,i2,exp_named_subst2)
+ ) ->
+ let b' = U.eq uri1 uri2 && i1 = i2 in
+ if b' then
+ (try
+ List.fold_right2
+ (fun (uri1,x) (uri2,y) (b,ugraph) ->
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
+ ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+ with
+ Invalid_argument _ -> false,ugraph
+ )
+ else
+ false,ugraph
+ | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
+ C.MutConstruct (uri2,i2,j2,exp_named_subst2)
+ ) ->
+ let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
+ if b' then
+ (try
+ List.fold_right2
+ (fun (uri1,x) (uri2,y) (b,ugraph) ->
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
+ ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+ with
+ Invalid_argument _ -> false,ugraph
+ )
+ else
+ false,ugraph
+ | (C.MutCase (uri1,i1,outtype1,term1,pl1),
+ C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
+ let b' = U.eq uri1 uri2 && i1 = i2 in
+ if b' then
+ let b'',ugraph''=aux test_equality_only context
+ outtype1 outtype2 ugraph in
+ if b'' then
+ let b''',ugraph'''= aux test_equality_only context
+ term1 term2 ugraph'' in
+ List.fold_right2
+ (fun x y (b,ugraph) ->
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph)
+ pl1 pl2 (true,ugraph''')
+ else
+ false,ugraph
+ else
+ false,ugraph
+ | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
+ let tys =
+ List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+ in
+ if i1 = i2 then
+ List.fold_right2
+ (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
+ if b && recindex1 = recindex2 then
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
+ | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
+ let tys =
+ List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+ in
+ if i1 = i2 then
+ List.fold_right2
+ (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
+ if b then
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
+ | (C.Cast _, _) | (_, C.Cast _)
+ | (C.Implicit _, _) | (_, C.Implicit _) ->
+ assert false
+ | (_,_) -> false,ugraph
+ end
+ in
+ begin
+ debug t1 [t2] "PREWHD";
+ (*
+ (match t1 with
+ Cic.Meta _ ->
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm (whd ~subst context t1));
+ prerr_endline (CicPp.ppterm t2);
+ prerr_endline (CicPp.ppterm (whd ~subst context t2))
+ | _ -> ()); *)
+ let t1' = whd ~subst context t1 in
+ let t2' = whd ~subst context t2 in
+ debug t1' [t2'] "POSTWHD";
+ aux2 test_equality_only t1' t2' ugraph
+ end
+ in
+ aux false (*c t1 t2 ugraph *)
+;;
+
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-(* TODO unify exceptions *)
-
-exception CicReductionInternalError;;
-exception WrongUriToInductiveDefinition;;
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
- let module C = Cic in
- let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
- if !fdebug = 0 then
- prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
-;;
-
-module type Strategy =
- sig
- type stack_term
- type env_term
- type ens_term
- val to_stack : Cic.term -> stack_term
- val to_stack_list : Cic.term list -> stack_term list
- val to_env : Cic.term -> env_term
- val to_ens : Cic.term -> ens_term
- val from_stack :
- unwind:
- (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> Cic.term) ->
- stack_term -> Cic.term
- val from_stack_list :
- unwind:
- (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> Cic.term) ->
- stack_term list -> Cic.term list
- val from_env : env_term -> Cic.term
- val from_ens : ens_term -> Cic.term
- val stack_to_env :
- reduce:
- (int * env_term list * ens_term Cic.explicit_named_substitution *
- Cic.term * stack_term list -> Cic.term) ->
- unwind:
- (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> Cic.term) ->
- stack_term -> env_term
- val compute_to_env :
- reduce:
- (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
- stack_term list -> Cic.term) ->
- unwind:
- (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> Cic.term) ->
- int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> env_term
- val compute_to_stack :
- reduce:
- (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
- stack_term list -> Cic.term) ->
- unwind:
- (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> Cic.term) ->
- int -> env_term list -> ens_term Cic.explicit_named_substitution ->
- Cic.term -> stack_term
- end
-;;
-
-module CallByNameStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- let to_stack v = v
- let to_stack_list l = l
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
- let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
- end
-;;
-
-module CallByValueStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- let to_stack v = v
- let to_stack_list l = l
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- end
-;;
-
-module CallByValueStrategyByNameOnConstants =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- let to_stack v = v
- let to_stack_list l = l
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- end
-;;
-
-module LazyCallByValueStrategy =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- let to_stack v = lazy v
- let to_stack_list l = List.map to_stack l
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByValueStrategyByNameOnConstants =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- let to_stack v = lazy v
- let to_stack_list l = List.map to_stack l
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[]))
- let compute_to_env ~reduce ~unwind k e ens t =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByNameStrategy =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- let to_stack v = lazy v
- let to_stack_list l = List.map to_stack l
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- end
-;;
-
-module
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
-=
- struct
- type stack_term = reduce:bool -> Cic.term
- type env_term = reduce:bool -> Cic.term
- type ens_term = reduce:bool -> Cic.term
- let to_stack v =
- let value = lazy v in
- fun ~reduce -> Lazy.force value
- let to_stack_list l = List.map to_stack l
- let to_env v =
- let value = lazy v in
- fun ~reduce -> Lazy.force value
- let to_ens v =
- let value = lazy v in
- fun ~reduce -> Lazy.force value
- let from_stack ~unwind v = (v ~reduce:false)
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = (v ~reduce:true)
- let from_ens v = (v ~reduce:true)
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t =
- let svalue =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- ) in
- let lvalue =
- lazy (unwind k e ens t)
- in
- fun ~reduce ->
- if reduce then Lazy.force svalue else Lazy.force lvalue
- let compute_to_env ~reduce ~unwind k e ens t =
- let svalue =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- ) in
- let lvalue =
- lazy (unwind k e ens t)
- in
- fun ~reduce ->
- if reduce then Lazy.force svalue else Lazy.force lvalue
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsStrategy =
- struct
- type stack_term =
- int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- let to_stack v = (0,[],[],v)
- let to_stack_list l = List.map to_stack l
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = v
- let from_ens v = v
- let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t =
- unwind k e ens t
- let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
- struct
- type stack_term =
- int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- let to_stack v = (0,[],[],v)
- let to_stack_list l = List.map to_stack l
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = v
- let from_ens v = v
- let stack_to_env ~reduce ~unwind (k,e,ens,t) =
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t =
- unwind k e ens t
- let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-module Reduction(RS : Strategy) =
- struct
- type env = RS.env_term list
- type ens = RS.ens_term Cic.explicit_named_substitution
- type stack = RS.stack_term list
- type config = int * env * ens * Cic.term * stack
-
- (* k is the length of the environment e *)
- (* m is the current depth inside the term *)
- let unwind' m k e ens t =
- let module C = Cic in
- let module S = CicSubstitution in
- if k = 0 && ens = [] then
- t
- else
- let rec unwind_aux m =
- function
- C.Rel n as t ->
- if n <= m then t else
- let d =
- try
- Some (RS.from_env (List.nth e (n-m-1)))
- with _ -> None
- in
- (match d with
- Some t' ->
- if m = 0 then t' else S.lift m t'
- | None -> C.Rel (n-k)
- )
- | C.Var (uri,exp_named_subst) ->
-(*
-prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
-*)
- if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
- CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
- else
- let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant _ -> raise ReferenceToConstant
- | C.Variable (_,_,_,params,_) -> params
- | C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- in
- let exp_named_subst' =
- substaux_in_exp_named_subst params exp_named_subst m
- in
- C.Var (uri,exp_named_subst')
- | C.Meta (i,l) ->
- let l' =
- List.map
- (function
- None -> None
- | Some t -> Some (unwind_aux m t)
- ) l
- in
- C.Meta (i, l')
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
- | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
- | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
- | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
- | C.Const (uri,exp_named_subst) ->
- let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant (_,_,_,params,_) -> params
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,_,_,params,_) -> params
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- in
- let exp_named_subst' =
- substaux_in_exp_named_subst params exp_named_subst m
- in
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,i,exp_named_subst) ->
- let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant _ -> raise ReferenceToConstant
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_,_) -> params
- )
- in
- let exp_named_subst' =
- substaux_in_exp_named_subst params exp_named_subst m
- in
- C.MutInd (uri,i,exp_named_subst')
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant _ -> raise ReferenceToConstant
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_,_) -> params
- )
- in
- let exp_named_subst' =
- substaux_in_exp_named_subst params exp_named_subst m
- in
- C.MutConstruct (uri,i,j,exp_named_subst')
- | C.MutCase (sp,i,outt,t,pl) ->
- C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
- List.map (unwind_aux m) pl)
- | C.Fix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) ->
- (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- and substaux_in_exp_named_subst params exp_named_subst' m =
- (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
- let ens' =
- List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
- (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
- List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
- in
- let rec filter_and_lift =
- function
- [] -> []
- | uri::tl ->
- let r = filter_and_lift tl in
- (try
- (uri,(List.assq uri ens'))::r
- with
- Not_found -> r
- )
- in
- filter_and_lift params
- *)
-
- (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
- (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
-
- (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
- (*CSC: codice altamente inefficiente *)
- let rec filter_and_lift already_instantiated =
- function
- [] -> []
- | (uri,t)::tl when
- List.for_all
- (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
- &&
- not (List.mem uri already_instantiated)
- &&
- List.mem uri params
- ->
- (uri,CicSubstitution.lift m (RS.from_ens t)) ::
- (filter_and_lift (uri::already_instantiated) tl)
- | _::tl -> filter_and_lift already_instantiated tl
-(*
- | (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
- filter_and_lift tl
-*)
- in
- List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
- (filter_and_lift [] (List.rev ens))
- in
- unwind_aux m t
- ;;
-
- let unwind =
- unwind' 0
- ;;
-
- let reduce ?(subst = []) context : config -> Cic.term =
- let module C = Cic in
- let module S = CicSubstitution in
- let rec reduce =
- function
- (k, e, _, (C.Rel n as t), s) ->
- let d =
- try
- Some (RS.from_env (List.nth e (n-1)))
- with
- _ ->
- try
- begin
- match List.nth context (n - 1 - k) with
- None -> assert false
- | Some (_,C.Decl _) -> None
- | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
- end
- with
- _ -> None
- in
- (match d with
- Some t' -> reduce (0,[],[],t',s)
- | None ->
- if s = [] then
- C.Rel (n-k)
- else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
- )
- | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
- if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
- reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
- else
- ( let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- match o with
- C.Constant _ -> raise ReferenceToConstant
- | C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_,_,_) ->
- let t' = unwind k e ens t in
- if s = [] then t' else
- C.Appl (t'::(RS.from_stack_list ~unwind s))
- | C.Variable (_,Some body,_,_,_) ->
- let ens' = push_exp_named_subst k e ens exp_named_subst in
- reduce (0, [], ens', body, s)
- )
- | (k, e, ens, (C.Meta (n,l) as t), s) ->
- (try
- let (_, term,_) = CicUtil.lookup_subst n subst in
- reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
- with CicUtil.Subst_not_found _ ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
- | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
- | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
- | (k, e, ens, (C.Cast (te,ty) as t), s) ->
- reduce (k, e, ens, te, s) (* s should be empty *)
- | (k, e, ens, (C.Prod _ as t), s) ->
- unwind k e ens t (* s should be empty *)
- | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
- | (k, e, ens, C.Lambda (_,_,t), p::s) ->
- reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
- | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
- let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
- reduce (k+1, m'::e, ens, t, s)
- | (_, _, _, C.Appl [], _) -> assert false
- | (k, e, ens, C.Appl (he::tl), s) ->
- let tl' =
- List.map
- (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
- in
- reduce (k, e, ens, he, (List.append tl') s)
- (* CSC: Old Dead Code
- | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
- | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
- | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
- | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
- (* strict evaluation, but constants are NOT unfolded *)
- let red =
- function
- C.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- in
- let tl' = List.map red tl in
- reduce (k, e, ens, he , List.append tl' s)
- | (k, e, ens, C.Appl l, s) ->
- C.Appl (List.append (List.map (unwind k e ens) l) s)
- *)
- | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
- (let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- match o with
- C.Constant (_,Some body,_,_,_) ->
- let ens' = push_exp_named_subst k e ens exp_named_subst in
- (* constants are closed *)
- reduce (0, [], ens', body, s)
- | C.Constant (_,None,_,_,_) ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_,_,_) ->
- let ens' = push_exp_named_subst k e ens exp_named_subst in
- (* constants are closed *)
- reduce (0, [], ens', body, s)
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- | (k, e, ens, (C.MutInd _ as t),s) ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
- | (k, e, ens, (C.MutConstruct _ as t),s) ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
- | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
- let decofix =
- function
- C.CoFix (i,fl) as t ->
- let (_,_,body) = List.nth fl i in
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
- fl
- body
- in
- (* the term is the result of a reduction; *)
- (* so it is already unwinded. *)
- reduce (0,[],[],body',[])
- | C.Appl (C.CoFix (i,fl) :: tl) ->
- let (_,_,body) = List.nth fl i in
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
- fl
- body
- in
- (* the term is the result of a reduction; *)
- (* so it is already unwinded. *)
- reduce (0,[],[],body',RS.to_stack_list tl)
- | t -> t
- in
- (match decofix (reduce (k,e,ens,term,[])) with
- C.MutConstruct (_,_,j,_) ->
- reduce (k, e, ens, (List.nth pl (j-1)), s)
- | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
- let (arity, r) =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
- in
- match o with
- C.InductiveDefinition (tl,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
- | _ -> raise WrongUriToInductiveDefinition
- in
- let ts =
- let num_to_eat = r in
- let rec eat_first =
- function
- (0,l) -> l
- | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
- | _ -> raise (Impossible 5)
- in
- eat_first (num_to_eat,tl)
- in
- (* ts are already unwinded because they are a sublist of tl *)
- reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
- | C.Cast _ | C.Implicit _ ->
- raise (Impossible 2) (* we don't trust our whd ;-) *)
- | _ ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
- )
- | (k, e, ens, (C.Fix (i,fl) as t), s) ->
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- Some (RS.from_stack ~unwind (List.nth s recindex))
- with
- _ -> None
- in
- (match recparam with
- Some recparam ->
- (match reduce (0,[],[],recparam,[]) with
- (* match recparam with *)
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- (* OLD
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
- fl
- body
- in
- reduce (k, e, ens, body', s) *)
- (* NEW *)
- let leng = List.length fl in
- let fl' =
- let unwind_fl (name,recindex,typ,body) =
- (name,recindex,unwind k e ens typ,
- unwind' leng k e ens body)
- in
- List.map unwind_fl fl
- in
- let new_env =
- let counter = ref 0 in
- let rec build_env e =
- if !counter = leng then e
- else
- (incr counter ;
- build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
- in
- build_env e
- in
- reduce (k+leng, new_env, ens, body, s)
- | _ ->
- let t' = unwind k e ens t in
- if s = [] then t' else
- C.Appl (t'::(RS.from_stack_list ~unwind s))
- )
- | None ->
- let t' = unwind k e ens t in
- if s = [] then t' else
- C.Appl (t'::(RS.from_stack_list ~unwind s))
- )
- | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
- and push_exp_named_subst k e ens =
- function
- [] -> ens
- | (uri,t)::tl ->
- push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
- in
- reduce
- ;;
- (*
- let rec whd context t =
- try
- reduce context (0, [], [], t, [])
- with Not_found ->
- prerr_endline (CicPp.ppterm t) ;
- raise Not_found
- ;;
- *)
-
- let rec whd ?(subst=[]) context t =
- reduce ~subst context (0, [], [], t, [])
- ;;
-
-
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
- if not (CicReductionNaif.are_convertible context res rescsc) then
- begin
- prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
- flush stderr ;
- prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
- flush stderr ;
- prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
- flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ = CicReductionNaif.are_convertible context res rescsc in
- assert false ;
- end
- else
- res
-;;
-*)
- end
-;;
-
-
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
-module R = Reduction
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
-module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
-*)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
-module U = UriManager;;
-
-let whd = R.whd;;
-
- (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
- * fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
-
-(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[]) =
- let rec aux test_equality_only context t1 t2 ugraph =
- let aux2 test_equality_only t1 t2 ugraph =
-
- (* this trivial euristic cuts down the total time of about five times ;-) *)
- (* this because most of the time t1 and t2 are "sintactically" the same *)
- if t1 === t2 then
- true,ugraph
- else
- begin
- let module C = Cic in
- match (t1,t2) with
- (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
- | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
- if U.eq uri1 uri2 then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- let b',ugraph' = aux test_equality_only context x y ugraph in
- (U.eq uri1 uri2 && b' && b),ugraph'
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
- if n1 = n2 then
- let b2, ugraph1 =
- let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
- let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
- List.fold_left2
- (fun (b,ugraph) t1 t2 ->
- if b then
- match t1,t2 with
- None,_
- | _,None -> true,ugraph
- | Some t1',Some t2' ->
- aux test_equality_only context t1' t2' ugraph
- else
- false,ugraph
- ) (true,ugraph) l1 l2
- in
- if b2 then true,ugraph1 else false,ugraph
- else
- false,ugraph
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- true,(CicUniv.add_eq t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- true,(CicUniv.add_ge t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
- | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let b',ugraph' = aux true context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only
- ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
- else
- false,ugraph
- | (C.Appl l1, C.Appl l2) ->
- (try
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph) l1 l2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
- let b' = U.eq uri1 uri2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutInd (uri1,i1,exp_named_subst1),
- C.MutInd (uri2,i2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
- C.MutConstruct (uri2,i2,j2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutCase (uri1,i1,outtype1,term1,pl1),
- C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- let b'',ugraph''=aux test_equality_only context
- outtype1 outtype2 ugraph in
- if b'' then
- let b''',ugraph'''= aux test_equality_only context
- term1 term2 ugraph'' in
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph)
- pl1 pl2 (true,ugraph''')
- else
- false,ugraph
- else
- false,ugraph
- | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
- let tys =
- List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
- if b && recindex1 = recindex2 then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
- let tys =
- List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
- if b then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit _, _) | (_, C.Implicit _) ->
- assert false
- | (_,_) -> false,ugraph
- end
- in
- begin
- debug t1 [t2] "PREWHD";
- (*
- (match t1 with
- Cic.Meta _ ->
- prerr_endline (CicPp.ppterm t1);
- prerr_endline (CicPp.ppterm (whd ~subst context t1));
- prerr_endline (CicPp.ppterm t2);
- prerr_endline (CicPp.ppterm (whd ~subst context t2))
- | _ -> ()); *)
- let t1' = whd ~subst context t1 in
- let t2' = whd ~subst context t2 in
- debug t1' [t2'] "POSTWHD";
- aux2 test_equality_only t1' t2' ugraph
- end
- in
- aux false (*c t1 t2 ugraph *)
-;;
-
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-exception WrongUriToInductiveDefinition
-exception ReferenceToConstant
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-val fdebug : int ref
-val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible : Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> bool * CicUniv.universe_graph
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-exception CicReductionInternalError;;
-exception WrongUriToInductiveDefinition;;
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
- let module C = Cic in
- let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
- if !fdebug = 0 then
- prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
-;;
-
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-exception RelToHiddenHypothesis;;
-
-(* takes a well-typed term *)
-let whd context =
- let rec whdaux l =
- let module C = Cic in
- let module S = CicSubstitution in
- function
- C.Rel n as t ->
- (match List.nth context (n-1) with
- Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
- )
- | C.Var (uri,exp_named_subst) as t ->
- let o,_ =
- CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant _ -> raise ReferenceToConstant
- | C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
- | C.Variable (_,Some body,_,_,_) ->
- whdaux l (CicSubstitution.subst_vars exp_named_subst body)
- )
- | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
- | C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit _ as t -> t
- | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
- | C.Prod _ as t -> t (* l should be empty *)
- | C.Lambda (name,s,t) as t' ->
- (match l with
- [] -> t'
- | he::tl -> whdaux tl (S.subst he t)
- (* when name is Anonimous the substitution should be superfluous *)
- )
- | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
- | C.Appl (he::tl) -> whdaux (tl@l) he
- | C.Appl [] -> raise (Impossible 1)
- | C.Const (uri,exp_named_subst) as t ->
- let o,_ =
- CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
- in
- (match o with
- C.Constant (_,Some body,_,_,_) ->
- whdaux l (CicSubstitution.subst_vars exp_named_subst body)
- | C.Constant _ -> if l = [] then t else C.Appl (t::l)
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_,_,_) ->
- whdaux l (CicSubstitution.subst_vars exp_named_subst body)
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l)
- | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l)
- | C.MutCase (mutind,i,_,term,pl) as t->
- let decofix =
- function
- C.CoFix (i,fl) as t ->
- let (_,_,body) = List.nth fl i in
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
- fl
- body
- in
- whdaux [] body'
- | C.Appl (C.CoFix (i,fl) :: tl) ->
- let (_,_,body) = List.nth fl i in
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
- fl
- body
- in
- whdaux tl body'
- | t -> t
- in
- (match decofix (whdaux [] term) with
- C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1))
- | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
- let (arity, r) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
- match o with
- C.InductiveDefinition (tl,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
- | _ -> raise WrongUriToInductiveDefinition
- in
- let ts =
- let rec eat_first =
- function
- (0,l) -> l
- | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
- | _ -> raise (Impossible 5)
- in
- eat_first (r,tl)
- in
- whdaux (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit _ ->
- raise (Impossible 2) (* we don't trust our whd ;-) *)
- | _ -> if l = [] then t else C.Appl (t::l)
- )
- | C.Fix (i,fl) as t ->
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- Some (List.nth l recindex)
- with
- _ -> None
- in
- (match recparam with
- Some recparam ->
- (match whdaux [] recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
- fl
- body
- in
- (* Possible optimization: substituting whd recparam in l *)
- whdaux l body'
- | _ -> if l = [] then t else C.Appl (t::l)
- )
- | None -> if l = [] then t else C.Appl (t::l)
- )
- | C.CoFix (i,fl) as t ->
- if l = [] then t else C.Appl (t::l)
- in
-(*CSC
-function t ->
-prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ;
-List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline "<PRIMA WHD" ; flush stderr ;
-let res =
-*)
- whdaux []
-(*CSC
-t in prerr_endline "DOPO WHD" ; flush stderr ; res
-*)
-;;
-
-(* t1, t2 must be well-typed *)
-let are_convertible c t1 t2 ugraph =
- let module U = UriManager in
- let rec aux test_equality_only context t1 t2 ugraph =
- let aux2 test_equality_only t1 t2 ugraph =
- (* this trivial euristic cuts down the total time of about five times ;-) *)
- (* this because most of the time t1 and t2 are "sintactically" the same *)
- if t1 = t2 then
- true,ugraph
- else
- begin
- let module C = Cic in
- match (t1,t2) with
- (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
- | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
- let b = U.eq uri1 uri2 in
- if b then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- (* FIXME: lazy! *)
- let b',ugraph' = aux test_equality_only context x y ugraph in
- (U.eq uri1 uri2 && b' && b),ugraph'
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
- let b = n1 = n2 in
- if b then
- List.fold_left2
- (fun (b,ugraph) t1 t2 ->
- if b then
- match t1,t2 with
- None,_
- | _,None -> true,ugraph
- | Some t1',Some t2' ->
- aux test_equality_only context t1' t2' ugraph
- else
- false,ugraph
- ) (true,ugraph) l1 l2
- else
- false,ugraph
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- true,(CicUniv.add_eq t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- true,(CicUniv.add_ge t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
- | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let b',ugraph' = aux true context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only
- ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
- else
- false,ugraph
- | (C.Appl l1, C.Appl l2) ->
- (try
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph) l1 l2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
- let b' = U.eq uri1 uri2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutInd (uri1,i1,exp_named_subst1),
- C.MutInd (uri2,i2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
- C.MutConstruct (uri2,i2,j2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutCase (uri1,i1,outtype1,term1,pl1),
- C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- let b'',ugraph''=aux test_equality_only context
- outtype1 outtype2 ugraph in
- if b'' then
- let b''',ugraph'''= aux test_equality_only context
- term1 term2 ugraph'' in
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph)
- pl1 pl2 (true,ugraph''')
- else
- false,ugraph
- else
- false,ugraph
- | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
- let tys =
- List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
- if b && recindex1 = recindex2 then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
- let tys =
- List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
- if b then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit _, _) | (_, C.Implicit _) ->
- assert false
- | (_,_) -> false,ugraph
- end
- in
- let b,ugraph' = aux2 test_equality_only t1 t2 ugraph in
- if b then
- b,ugraph'
- else
- begin
- debug t1 [t2] "PREWHD";
- let t1' = whd context t1 in
- let t2' = whd context t2 in
- debug t1' [t2'] "POSTWHD";
- aux2 test_equality_only t1' t2' ugraph
- end
- in
- aux false c t1 t2 ugraph
-;;
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-exception WrongUriToInductiveDefinition
-exception ReferenceToConstant
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-val fdebug : int ref
-val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible :
- Cic.context -> Cic.term -> Cic.term ->
- CicUniv.universe_graph -> bool * CicUniv.universe_graph
substaux 1
;;
-(* lift_meta [t_1 ; ... ; t_n] t *)
+(* subst_meta [t_1 ; ... ; t_n] t *)
(* returns the term [t] where [Rel i] is substituted with [t_i] *)
(* [t_i] is lifted as usual when it crosses an abstraction *)
-let lift_meta l t =
+let subst_meta l t =
let module C = Cic in
if l = [] then t else
let rec aux k = function
val subst_vars :
Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term
-(* TODO CSC rename to subst_meta *)
-
-(* lift_meta [t_1 ; ... ; t_n] t *)
+(* subst_meta [t_1 ; ... ; t_n] t *)
(* returns the term [t] where [Rel i] is substituted with [t_i] *)
(* [t_i] is lifted as usual when it crosses an abstraction *)
-val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term
+val subst_meta : (Cic.term option) list -> Cic.term -> Cic.term
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
in
aux 1 canonical_context
in
~subst metasenv context canonical_context l ugraph
in
(* assuming subst is well typed !!!!! *)
- ((CicSubstitution.lift_meta l ty), ugraph1)
- (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+ ((CicSubstitution.subst_meta l ty), ugraph1)
+ (* type_of_aux context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let ugraph1 =
check_metasenv_consistency ~logger
~subst metasenv context canonical_context l ugraph
in
- ((CicSubstitution.lift_meta l ty),ugraph1))
+ ((CicSubstitution.subst_meta l ty),ugraph1))
(* TASSI: CONSTRAINTS *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
(* when an 'ident option is None, the default is to apply the tactic
to the current goal *)
-type ('term, 'ident) tactic =
- | LocatedTactic of CicAst.location * ('term, 'ident) tactic
+type loc = CicAst.location
- | Absurd of 'term
- | Apply of 'term
- | Auto
- | Assumption
- | Change of 'term * 'term * 'ident option (* what, with what, where *)
- | Change_pattern of 'term pattern * 'term * 'ident option
+type ('term, 'ident) tactic =
+ | Absurd of loc * 'term
+ | Apply of loc * 'term
+ | Auto of loc
+ | Assumption of loc
+ | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
+ | Change_pattern of loc * 'term pattern * 'term * 'ident option
(* what, with what, where *)
- | Contradiction
- | Cut of 'term
- | Decompose of 'ident * 'ident list (* where, which principles *)
- | Discriminate of 'ident
- | Elim of 'term * 'term option (* what to elim, which principle to use *)
- | ElimType of 'term
- | Exact of 'term
- | Exists
- | Fold of reduction_kind * 'term
- | Fourier
- | Hint
- | Injection of 'ident
- | Intros of int option * 'ident list
- | Left
- | LetIn of 'term * 'ident
-(* | Named_intros of 'ident list (* joined with Intros above *) *)
-(* | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *)
- | Reduce of reduction_kind * ('term list * 'term pattern) option
+ | Contradiction of loc
+ | Cut of loc * 'term
+ | Decompose of loc * 'ident * 'ident list (* where, which principles *)
+ | Discriminate of loc * 'ident
+ | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
+ | ElimType of loc * 'term
+ | Exact of loc * 'term
+ | Exists of loc
+ | Fold of loc * reduction_kind * 'term
+ | Fourier of loc
+ | Goal of loc * int (* change current goal, argument is goal number 1-based *)
+ | Hint of loc
+ | Injection of loc * 'ident
+ | Intros of loc * int option * 'ident list
+ | Left of loc
+ | LetIn of loc * 'term * 'ident
+(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
+(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+ | Reduce of loc * reduction_kind * ('term list * 'term pattern) option
(* kind, (what, where)
* if second argument is None, reduction is applied to the current goal,
- * otherwise to each occurrence of terms given in list occuring in term
+ * otherwise to each occurrence of loc * terms given in list occuring in term
* pattern *)
- | Reflexivity
- | Replace of 'term * 'term (* what, with what *)
- | Replace_pattern of 'term pattern * 'term
- | Rewrite of direction * 'term * 'ident option
- | Right
- | Ring
- | Split
- | Symmetry
- | Transitivity of 'term
+ | Reflexivity of loc
+ | Replace of loc * 'term * 'term (* what, with what *)
+ | Replace_pattern of loc * 'term pattern * 'term
+ | Rewrite of loc * direction * 'term * 'ident option
+ | Right of loc
+ | Ring of loc
+ | Split of loc
+ | Symmetry of loc
+ | Transitivity of loc * 'term
type thm_flavour =
[ `Definition
| `Fact
- | `Goal
| `Lemma
| `Remark
| `Theorem
type print_kind = [ `Env | `Coer ]
+type 'term macro =
+ | Abort of loc
+ | Print of loc * string
+ | Check of loc * 'term
+ | Quit of loc
+ | Redo of loc * int option
+ | Undo of loc * int option
+(* | Print of loc * print_kind *)
+ | Search_pat of loc * search_kind * string (* searches with string pattern *)
+ | Search_term of loc * search_kind * 'term (* searches with term pattern *)
+
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
type 'term command =
- | Abort
- | Baseuri of string option (** get/set base uri *)
- | Basedir of string option (** get/set base dir *)
- | Check of 'term
- | Search_pat of search_kind * string (* searches with string pattern *)
- | Search_term of search_kind * 'term (* searches with term pattern *)
- | Proof
- | Qed of string option
+ | Set of loc * string * string
+ | Qed of loc
(** name.
* Name is needed when theorem was started without providing a name
*)
- | Quit
- | Inductive of (string * 'term) list * 'term inductive_type list
- (** parameters, list of mutual inductive types *)
- | Theorem of thm_flavour * string option * 'term * 'term option
+ | Inductive of loc * (string * 'term) list * 'term inductive_type list
+ (** parameters, list of loc * mutual inductive types *)
+ | Theorem of loc * thm_flavour * string option * 'term * 'term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
- | Coercion of 'term
- | Redo of int option
- | Undo of int option
- | Print of print_kind
+ | Coercion of loc * 'term
+ | Alias of loc * alias_spec
type ('term, 'ident) tactical =
- | LocatedTactical of CicAst.location * ('term, 'ident) tactical
-
- | Tactic of ('term, 'ident) tactic
- | Command of 'term command
+ | Tactic of loc * ('term, 'ident) tactic
+ | Fail of loc
+ | Do of loc * int * ('term, 'ident) tactical
+ | IdTac of loc
+ | Repeat of loc * ('term, 'ident) tactical
+ | Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
+ | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list
+ | Tries of loc * ('term, 'ident) tactical list
+ (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
+ | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
- | Fail
- | Do of int * ('term, 'ident) tactical
- | IdTac
- | Repeat of ('term, 'ident) tactical
- | Seq of ('term, 'ident) tactical list (* sequential composition *)
- | Then of ('term, 'ident) tactical * ('term, 'ident) tactical list
- | Tries of ('term, 'ident) tactical list
- (* try a sequence of tacticals until one succeeds, fail otherwise *)
- | Try of ('term, 'ident) tactical (* try a tactical and mask failures *)
+type ('term, 'ident) statement =
+ | Command of loc * 'term command
+ | Macro of loc * 'term macro
+ (* Macro are substantially queries, but since we are not the kind of
+ * peolpe that like to push "start" to turn off the computer
+ * we added this command *)
+ | Tactical of loc * ('term, 'ident) tactical
let rec count_tactic current_size tac =
if current_size > maxsize then current_size
else match tac with
- LocatedTactic (_, tac) -> count_tactic current_size tac
- | Absurd term -> countterm (current_size + 6) term
- | Apply term -> countterm (current_size + 6) term
- | Auto -> current_size + 4
- | Assumption -> current_size + 10
- | Change (t1, t2, where) ->
+ | Absurd (_, term) -> countterm (current_size + 6) term
+ | Apply (_, term) -> countterm (current_size + 6) term
+ | Auto _ -> current_size + 4
+ | Assumption _ -> current_size + 10
+ | Change (_, t1, t2, where) ->
let size1 = countterm (current_size + 12) t1 in (* change, with *)
let size2 = countterm size1 t2 in
(match where with
None -> size2
| Some ident -> size2 + 3 + String.length ident)
- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> current_size + 13
- | Cut term -> countterm (current_size + 4) term
- | Decompose (ident, principles) ->
+ | Change_pattern _ -> assert false (* TODO *)
+ | Contradiction _ -> current_size + 13
+ | Cut (_, term) -> countterm (current_size + 4) term
+ | Decompose (_, ident, principles) ->
List.fold_left
(fun size s -> size + (String.length s))
(current_size + 11 + String.length ident) principles
- | Discriminate ident -> current_size + 12 + (String.length ident)
- | Elim (term, using) ->
+ | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
+ | Elim (_, term, using) ->
let size1 = countterm (current_size + 5) term in
(match using with
None -> size1
| Some term -> countterm (size1 + 7) term)
- | ElimType term -> countterm (current_size + 10) term
- | Exact term -> countterm (current_size + 6) term
- | Exists -> current_size + 6
- | Fold (kind, term) ->
+ | ElimType (_, term) -> countterm (current_size + 10) term
+ | Exact (_, term) -> countterm (current_size + 6) term
+ | Exists _ -> current_size + 6
+ | Fold (_, kind, term) ->
countterm (current_size + 5) term
- | Fourier -> current_size + 7
- | Hint -> current_size + 4
- | Injection ident -> current_size + 10 + (String.length ident)
- | Intros (num, idents) ->
+ | Fourier _ -> current_size + 7
+ | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
+ | Hint _ -> current_size + 4
+ | Injection (_, ident) -> current_size + 10 + (String.length ident)
+ | Intros (_, num, idents) ->
List.fold_left
(fun size s -> size + (String.length s))
(current_size + 7) idents
- | Left -> current_size + 4
- | LetIn (term, ident) ->
+ | Left _ -> current_size + 4
+ | LetIn (_, term, ident) ->
countterm (current_size + 5 + String.length ident) term
- | Reduce (_, _) -> assert false (* TODO *)
- | Reflexivity -> current_size + 11
- | Replace (t1, t2) ->
+ | Reduce _ -> assert false (* TODO *)
+ | Reflexivity _ -> current_size + 11
+ | Replace (_, t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
countterm size1 t2
- | Replace_pattern (_, _) -> assert false (* TODO *)
- | Rewrite (_, _, _) -> assert false (* TODO *)
- | Right -> current_size + 5
- | Ring -> current_size + 4
- | Split -> current_size + 5
- | Symmetry -> current_size + 8
- | Transitivity term ->
+ | Replace_pattern _ -> assert false (* TODO *)
+ | Rewrite _ -> assert false (* TODO *)
+ | Right _ -> current_size + 5
+ | Ring _ -> current_size + 4
+ | Split _ -> current_size + 5
+ | Symmetry _ -> current_size + 8
+ | Transitivity (_, term) ->
countterm (current_size + 13) term
;;
small_tactic2box tac
and big_tactic2box = function
- LocatedTactic (loc, tac) ->
- big_tactic2box tac
- | Absurd term ->
+ | Absurd (_, term) ->
Box.V([],[Box.Text([],"absurd");
ast2astBox term])
- | Apply term ->
+ | Apply (_, term) ->
Box.V([],[Box.Text([],"apply");
ast2astBox term])
- | Assumption -> Box.Text([],"assumption")
- | Auto -> Box.Text([],"auto")
- | Change (t1, t2, where) ->
+ | Assumption _ -> Box.Text([],"assumption")
+ | Auto _ -> Box.Text([],"auto")
+ | Change (_, t1, t2, where) ->
let where =
(match where with
None -> []
(pretty_append
[Box.Text([],"with")]
t2)@where)
- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> Box.Text([],"contradiction")
- | Cut term ->
+ | Change_pattern _ -> assert false (* TODO *)
+ | Contradiction _ -> Box.Text([],"contradiction")
+ | Cut (_, term) ->
Box.V([],[Box.Text([],"cut");
Box.indent(ast2astBox term)])
- | Decompose (ident, principles) ->
+ | Decompose (_, ident, principles) ->
let principles =
List.map (fun x -> Box.Text([],x)) principles in
Box.V([],[Box.Text([],"decompose");
Box.V([],principles);
Box.Text([],"]")]);
Box.Text([],ident)])
- | Discriminate ident ->
+ | Discriminate (_, ident) ->
Box.V([],[Box.Text([],"discriminate");
Box.Text([],ident)])
- | Elim (term, using) ->
+ | Elim (_, term, using) ->
let using =
(match using with
None -> []
(pretty_append
[Box.Text([],"elim")]
term)@using)
- | ElimType term ->
+ | ElimType (_, term) ->
Box.V([],[Box.Text([],"elim type");
Box.indent(ast2astBox term)])
- | Exact term ->
+ | Exact (_, term) ->
Box.V([],[Box.Text([],"exact");
Box.indent(ast2astBox term)])
- | Exists -> Box.Text([],"exists")
- | Fold (kind, term) ->
+ | Exists _ -> Box.Text([],"exists")
+ | Fold (_, kind, term) ->
Box.V([],[Box.H([],[Box.Text([],"fold");
Box.smallskip;
Box.Text([],string_of_kind kind)]);
Box.indent(ast2astBox term)])
- | Fourier -> Box.Text([],"fourier")
- | Hint -> Box.Text([],"hint")
- | Injection ident ->
+ | Fourier _ -> Box.Text([],"fourier")
+ | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
+ | Hint _ -> Box.Text([],"hint")
+ | Injection (_, ident) ->
Box.V([],[Box.Text([],"transitivity");
Box.indent (Box.Text([],ident))])
- | Intros (num, idents) ->
+ | Intros (_, num, idents) ->
let num =
(match num with
None -> []
Box.V([],[Box.Text([],"decompose");
Box.H([],[Box.smallskip;
Box.V([],idents)])])
- | Left -> Box.Text([],"left")
- | LetIn (term, ident) ->
+ | Left _ -> Box.Text([],"left")
+ | LetIn (_, term, ident) ->
Box.V([],[Box.H([],[Box.Text([],"let");
Box.smallskip;
Box.Text([],ident);
Box.smallskip;
Box.Text([],"=")]);
Box.indent (ast2astBox term)])
- | Reduce (_, _) -> assert false (* TODO *)
- | Reflexivity -> Box.Text([],"reflexivity")
- | Replace (t1, t2) ->
+ | Reduce _ -> assert false (* TODO *)
+ | Reflexivity _ -> Box.Text([],"reflexivity")
+ | Replace (_, t1, t2) ->
Box.V([],
(pretty_append
[Box.Text([],"replace")]
(pretty_append
[Box.Text([],"with")]
t2))
- | Replace_pattern (_, _) -> assert false (* TODO *)
- | Rewrite (_, _, _) -> assert false (* TODO *)
- | Right -> Box.Text([],"right")
- | Ring -> Box.Text([],"ring")
- | Split -> Box.Text([],"split")
- | Symmetry -> Box.Text([],"symmetry")
- | Transitivity term ->
+ | Replace_pattern _ -> assert false (* TODO *)
+ | Rewrite _ -> assert false (* TODO *)
+ | Right _ -> Box.Text([],"right")
+ | Ring _ -> Box.Text([],"ring")
+ | Split _ -> Box.Text([],"split")
+ | Symmetry _ -> Box.Text([],"symmetry")
+ | Transitivity (_, term) ->
Box.V([],[Box.Text([],"transitivity");
Box.indent (ast2astBox term)])
;;
open TacticAst
let rec tactical2box = function
- | LocatedTactical (loc, tac) -> tactical2box tac
-
- | Tactic tac -> tactic2box tac
+ | Tactic (_, tac) -> tactic2box tac
+(*
| Command cmd -> (* TODO dummy implementation *)
Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+*)
- | Fail -> Box.Text([],"fail")
- | Do (count, tac) ->
+ | Fail _ -> Box.Text([],"fail")
+ | Do (_, count, tac) ->
Box.V([],[Box.Text([],"do " ^ string_of_int count);
Box.indent (tactical2box tac)])
- | IdTac -> Box.Text([],"id")
- | Repeat tac ->
+ | IdTac _ -> Box.Text([],"id")
+ | Repeat (_, tac) ->
Box.V([],[Box.Text([],"repeat");
Box.indent (tactical2box tac)])
- | Seq tacs ->
+ | Seq (_, tacs) ->
Box.V([],tacticals2box tacs)
- | Then (tac, tacs) ->
+ | Then (_, tac, tacs) ->
Box.V([],[tactical2box tac;
Box.H([],[Box.skip;
Box.Text([],"[");
Box.V([],tacticals2box tacs);
Box.Text([],"]");])])
- | Tries tacs ->
+ | Tries (_, tacs) ->
Box.V([],[Box.Text([],"try");
Box.H([],[Box.skip;
Box.Text([],"[");
Box.V([],tacticals2box tacs);
Box.Text([],"]");])])
- | Try tac ->
+ | Try (_, tac) ->
Box.V([],[Box.Text([],"try");
Box.indent (tactical2box tac)])
open TacticAst
let tactical_terminator = "."
+let tactic_terminator = tactical_terminator
let tactical_separator = ";"
-let pp_term term = CicAstPp.pp_term term
+let pp_term_ast term = CicAstPp.pp_term term
+let pp_term_cic term = CicPp.ppterm term
let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
| `Whd -> "whd"
let rec pp_tactic = function
- | LocatedTactic (loc, tac) -> pp_tactic tac
- | Absurd term -> "absurd" ^ pp_term term
- | Apply term -> "apply " ^ pp_term term
- | Auto -> "auto"
- | Assumption -> "assumption"
- | Change (t1, t2, where) ->
- sprintf "change %s with %s%s" (pp_term t1) (pp_term t2)
+ | Absurd (_, term) -> "absurd" ^ pp_term_ast term
+ | Apply (_, term) -> "apply " ^ pp_term_ast term
+ | Auto _ -> "auto"
+ | Assumption _ -> "assumption"
+ | Change (_, t1, t2, where) ->
+ sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2)
(match where with None -> "" | Some ident -> "in " ^ ident)
- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> "contradiction"
- | Cut term -> "cut " ^ pp_term term
- | Decompose (ident, principles) ->
+ | Change_pattern (_, _, _, _) -> assert false (* TODO *)
+ | Contradiction _ -> "contradiction"
+ | Cut (_, term) -> "cut " ^ pp_term_ast term
+ | Decompose (_, ident, principles) ->
sprintf "decompose %s %s" (pp_idents principles) ident
- | Discriminate ident -> "discriminate " ^ ident
- | Elim (term, using) ->
- sprintf "elim " ^ pp_term term ^
- (match using with None -> "" | Some term -> " using " ^ pp_term term)
- | ElimType term -> "elim type " ^ pp_term term
- | Exact term -> "exact " ^ pp_term term
- | Exists -> "exists"
- | Fold (kind, term) ->
- sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
- | Fourier -> "fourier"
- | Hint -> "hint"
- | Injection ident -> "injection " ^ ident
- | Intros (None, []) -> "intro"
- | Intros (num, idents) ->
+ | Discriminate (_, ident) -> "discriminate " ^ ident
+ | Elim (_, term, using) ->
+ sprintf "elim " ^ pp_term_ast term ^
+ (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+ | ElimType (_, term) -> "elim type " ^ pp_term_ast term
+ | Exact (_, term) -> "exact " ^ pp_term_ast term
+ | Exists _ -> "exists"
+ | Fold (_, kind, term) ->
+ sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
+ | Goal (_, n) -> "goal " ^ string_of_int n
+ | Fourier _ -> "fourier"
+ | Hint _ -> "hint"
+ | Injection (_, ident) -> "injection " ^ ident
+ | Intros (_, None, []) -> "intro"
+ | Intros (_, num, idents) ->
sprintf "intros%s%s"
(match num with None -> "" | Some num -> " " ^ string_of_int num)
(match idents with [] -> "" | idents -> " " ^ pp_idents idents)
- | Left -> "left"
- | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
- | Reduce (kind, None)
- | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind
- | Reduce (kind, Some ([], `Everywhere)) ->
+ | Left _ -> "left"
+ | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
+ | Reduce (_, kind, None)
+ | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind
+ | Reduce (_, kind, Some ([], `Everywhere)) ->
sprintf "%s in hyp" (pp_reduction_kind kind)
- | Reduce (kind, Some (terms, `Goal)) ->
+ | Reduce (_, kind, Some (terms, `Goal)) ->
sprintf "%s %s" (pp_reduction_kind kind)
- (String.concat ", " (List.map pp_term terms))
- | Reduce (kind, Some (terms, `Everywhere)) ->
+ (String.concat ", " (List.map pp_term_ast terms))
+ | Reduce (_, kind, Some (terms, `Everywhere)) ->
sprintf "%s in hyp %s" (pp_reduction_kind kind)
- (String.concat ", " (List.map pp_term terms))
- | Reflexivity -> "reflexivity"
- | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
- | Replace_pattern (_, _) -> assert false (* TODO *)
- | Rewrite (_, _, _) -> assert false (* TODO *)
- | Right -> "right"
- | Ring -> "ring"
- | Split -> "split"
- | Symmetry -> "symmetry"
- | Transitivity term -> "transitivity " ^ pp_term term
+ (String.concat ", " (List.map pp_term_ast terms))
+ | Reflexivity _ -> "reflexivity"
+ | Replace (_, t1, t2) ->
+ sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
+ | Replace_pattern (_, _, _) -> assert false (* TODO *)
+ | Rewrite (_, _, _, _) -> assert false (* TODO *)
+ | Right _ -> "right"
+ | Ring _ -> "ring"
+ | Split _ -> "split"
+ | Symmetry _ -> "symmetry"
+ | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
let pp_flavour = function
| `Definition -> "Definition"
| `Match -> "match"
| `Elim -> "elim"
-let pp_command = function
- | Abort -> "Abort"
- | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
- | Baseuri None -> "Baseuri"
- | Check term -> sprintf "Check %s" (pp_term term)
- | Proof -> "Proof"
- | Qed name ->
- (match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
- | Quit -> "Quit"
- | Redo None -> "Redo"
- | Redo (Some n) -> sprintf "Redo %d" n
- | Search_pat (kind, pat) ->
+let pp_macro pp_term = function
+ | Abort _ -> "Abort"
+ | Check (_, term) -> sprintf "Check %s" (pp_term term)
+ | Redo (_, None) -> "Redo"
+ | Redo (_, Some n) -> sprintf "Redo %d" n
+ | Search_pat (_, kind, pat) ->
sprintf "search %s \"%s\"" (pp_search_kind kind) pat
- | Search_term (kind, term) ->
+ | Search_term (_, kind, term) ->
sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
- | Inductive (params, types) ->
+ | Undo (_, None) -> "Undo"
+ | Undo (_, Some n) -> sprintf "Undo %d" n
+ | Print (_, name) -> sprintf "Print \"%s\"" name
+ | Quit _ -> "Quit"
+
+let pp_macro_ast = pp_macro pp_term_ast
+let pp_macro_cic = pp_macro pp_term_cic
+
+let pp_alias = function
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+ | Symbol_alias (symb, instance, desc) ->
+ sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
+ symb instance desc
+ | Number_alias (instance,desc) ->
+ sprintf "alias num (instance %d) = \"%s\"" instance desc
+
+let pp_command = function
+ | Qed _ -> "Qed"
+ | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
+ | Inductive (_, params, types) ->
let pp_params = function
| [] -> ""
| params ->
" " ^
String.concat " "
(List.map
- (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
+ (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
params)
in
let pp_constructors constructors =
String.concat "\n"
- (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
+ (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
constructors)
in
let pp_type (name, _, typ, constructors) =
- sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
+ sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ)
(pp_constructors constructors)
in
(match types with
let fst_typ_pp =
sprintf "%sinductive %s%s: %s \\def\n%s"
(if inductive then "" else "co") name (pp_params params)
- (pp_term typ) (pp_constructors constructors)
+ (pp_term_ast typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Theorem (flavour, name, typ, body) ->
+ | Theorem (_, flavour, name, typ, body) ->
sprintf "%s %s: %s %s"
(pp_flavour flavour)
(match name with None -> "" | Some name -> name)
- (pp_term typ)
+ (pp_term_ast typ)
(match body with
| None -> ""
- | Some body -> "\\def " ^ pp_term body)
- | Undo None -> "Undo"
- | Undo (Some n) -> sprintf "Undo %d" n
+ | Some body -> "\\def " ^ pp_term_ast body)
+ | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
+ | Alias (_,s) -> pp_alias s
let rec pp_tactical = function
- | LocatedTactical (loc, tac) -> pp_tactical tac
-
- | Tactic tac -> pp_tactic tac
- | Command cmd -> pp_command cmd
-
- | Fail -> "fail"
- | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
- | IdTac -> "id"
- | Repeat tac -> "repeat " ^ pp_tactical tac
- | Seq tacs -> pp_tacticals tacs
- | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
- | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs)
- | Try tac -> "try " ^ pp_tactical tac
+ | Tactic (_, tac) -> pp_tactic tac
+
+ | Fail _ -> "fail"
+ | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
+ | IdTac _ -> "id"
+ | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
+ | Seq (_, tacs) -> pp_tacticals tacs
+ | Then (_, tac, tacs) ->
+ sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
+ | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+ | Try (_, tac) -> "try " ^ pp_tactical tac
and pp_tacticals tacs =
String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs)
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
+let pp_tactic tac = pp_tactic tac ^ tactic_terminator
*)
val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-
+val pp_command: CicAst.term TacticAst.command -> string
+val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string
+val pp_macro_ast: CicAst.term TacticAst.macro -> string
+val pp_macro_cic: Cic.term TacticAst.macro -> string
val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
+val pp_alias: TacticAst.alias_spec -> string
Cic.Meta(n,l) as t ->
(try
deref subst
- (CicSubstitution.lift_meta
+ (CicSubstitution.subst_meta
l (third (CicUtil.lookup_subst n subst)))
with
CicUtil.Subst_not_found _ -> t)
| C.Meta (i, l) ->
(try
let (_, t,_) = lookup_subst i subst in
- um_aux (S.lift_meta l t)
+ um_aux (S.subst_meta l t)
with CicUtil.Subst_not_found _ ->
(* unconstrained variable, i.e. free in subst*)
let l' =
| C.Meta (i, l1) as t ->
(try
let (_,t,_) = CicUtil.lookup_subst i subst in
- deliftaux k (CicSubstitution.lift_meta l1 t)
+ deliftaux k (CicSubstitution.subst_meta l1 t)
with CicUtil.Subst_not_found _ ->
(* see the top level invariant *)
if (i = n) then
canonical_context l ugraph
in
(* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv', ugraph1
(* type_of_aux subst metasenv
- context (CicSubstitution.lift_meta l term) *)
+ context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let l',subst',metasenv', ugraph1 =
check_metasenv_consistency n subst metasenv context
canonical_context l ugraph
in
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
(Some (n,
- C.Def ((S.lift_meta l (S.lift i t)),
- Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ C.Def ((S.subst_meta l (S.lift i t)),
+ Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
Cic.Meta(n,l) as t ->
(try
deref subst
- (CicSubstitution.lift_meta
+ (CicSubstitution.subst_meta
l (snd (CicUtil.lookup_subst n subst)))
with
CicUtil.Subst_not_found _ -> t)
| C.Meta (i,l) as t->
(try
let (_, t') = CicMetaSubst.lookup_subst i subst in
- aux metasenv subst n context (CicSubstitution.lift_meta l t')
+ aux metasenv subst n context (CicSubstitution.subst_meta l t')
ugraph
with CicMetaSubst.SubstNotFound _ ->
let (subst, metasenv, context, local_context,ugraph1) =
begin
try
let (_, oldt) = CicMetaSubst.lookup_subst n subst in
- let lifted_oldt = S.lift_meta l oldt in
+ let lifted_oldt = S.subst_meta l oldt in
let ty_lifted_oldt,ugraph1 =
type_of_aux' metasenv subst context lifted_oldt ugraph
in
let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
fo_unif_subst
test_equality_only
- subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+ subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
with AssertFailure _ ->
(* TODO huge hack!!!!
* we keep on unifying/refining in the hope that the problem will be
(* Unifying the types may have already instantiated n. Let's check *)
try
let (_, oldt) = CicMetaSubst.lookup_subst n subst in
- let lifted_oldt = S.lift_meta l oldt in
+ let lifted_oldt = S.subst_meta l oldt in
fo_unif_subst_ordered
test_equality_only subst context metasenv t lifted_oldt ugraph2
with
in
fo_unif_subst
test_equality_only
- subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+ subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
with
UnificationFailure msg
| Uncertain msg ->
(* Unifying the types may have already instantiated n. Let's check *)
try
let (_, oldt,_) = CicUtil.lookup_subst n subst in
- let lifted_oldt = S.lift_meta l oldt in
+ let lifted_oldt = S.subst_meta l oldt in
fo_unif_subst_ordered
test_equality_only subst context metasenv t lifted_oldt ugraph2
with
*)
(try
let (_,t,_) = CicUtil.lookup_subst i subst in
- let lifted = S.lift_meta l t in
+ let lifted = S.subst_meta l t in
let reduced = beta_reduce (Cic.Appl (lifted::args)) in
fo_unif_subst
test_equality_only
| _, C.Meta (i,l)::args when not(exists_a_meta args) ->
(try
let (_,t,_) = CicUtil.lookup_subst i subst in
- let lifted = S.lift_meta l t in
+ let lifted = S.subst_meta l t in
let reduced = beta_reduce (Cic.Appl (lifted::args)) in
fo_unif_subst
test_equality_only
open Printf;;
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
+
(* the list of known coercions (MUST be transitively closed) *)
let coercions = ref [
(UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
- UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
+ UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
(
UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
* http://cs.unibo.it/helm/.
*)
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
+
val look_for_coercion :
UriManager.uri -> UriManager.uri -> Cic.term option
PACKAGE = hbugs
REQUIRES = \
pcre lablgtk2.glade \
- helm-thread helm-xml helm-pxp helm-tactics
+ helm-thread helm-xml helm-pxp helm-tactics helm-registry
IMPLEMENTATION_FILES = \
hbugs_misc.ml \
let debug = true ;;
let debug_print s = if debug then prerr_endline s ;;
-Http_common.debug := false;;
let daemon_name = "H-Bugs Broker" ;;
let default_port = 49081 ;;
open Printf;;
let rec string_of_hint = function
- | Use_ring_Luke -> "Use Ring, Luke!"
- | Use_fourier_Luke -> "Use Fourier, Luke!"
- | Use_reflexivity_Luke -> "Use reflexivity, Luke!"
- | Use_symmetry_Luke -> "Use symmetry, Luke!"
- | Use_assumption_Luke -> "Use assumption, Luke!"
- | Use_contradiction_Luke -> "Use contradiction, Luke!"
- | Use_exists_Luke -> "Use exists, Luke!"
- | Use_split_Luke -> "Use split, Luke!"
- | Use_left_Luke -> "Use left, Luke!"
- | Use_right_Luke -> "Use right, Luke!"
- | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term
+ | Use_ring -> "Use Ring, Luke!"
+ | Use_fourier -> "Use Fourier, Luke!"
+ | Use_reflexivity -> "Use reflexivity, Luke!"
+ | Use_symmetry -> "Use symmetry, Luke!"
+ | Use_assumption -> "Use assumption, Luke!"
+ | Use_contradiction -> "Use contradiction, Luke!"
+ | Use_exists -> "Use exists, Luke!"
+ | Use_split -> "Use split, Luke!"
+ | Use_left -> "Use left, Luke!"
+ | Use_right -> "Use right, Luke!"
+ | Use_apply term -> sprintf "Apply %s, Luke!" term
| Hints hints -> String.concat "; " (List.map string_of_hint hints)
;;
let parse_hint node =
let rec parse_hint_node node =
match node#node_type with
- | T_element "ring" -> Use_ring_Luke
- | T_element "fourier" -> Use_fourier_Luke
- | T_element "reflexivity" -> Use_reflexivity_Luke
- | T_element "symmetry" -> Use_symmetry_Luke
- | T_element "assumption" -> Use_assumption_Luke
- | T_element "contradiction" -> Use_contradiction_Luke
- | T_element "exists" -> Use_exists_Luke
- | T_element "split" -> Use_split_Luke
- | T_element "left" -> Use_left_Luke
- | T_element "right" -> Use_right_Luke
- | T_element "apply" -> Use_apply_Luke node#data
+ | T_element "ring" -> Use_ring
+ | T_element "fourier" -> Use_fourier
+ | T_element "reflexivity" -> Use_reflexivity
+ | T_element "symmetry" -> Use_symmetry
+ | T_element "assumption" -> Use_assumption
+ | T_element "contradiction" -> Use_contradiction
+ | T_element "exists" -> Use_exists
+ | T_element "split" -> Use_split
+ | T_element "left" -> Use_left
+ | T_element "right" -> Use_right
+ | T_element "apply" -> Use_apply node#data
| T_element "hints" ->
Hints
(List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
| None -> "<gTopLevelStatus />\n"
let rec pp_hint = function
- | Use_ring_Luke -> sprintf "<ring />"
- | Use_fourier_Luke -> sprintf "<fourier />"
- | Use_reflexivity_Luke -> sprintf "<reflexivity />"
- | Use_symmetry_Luke -> sprintf "<symmetry />"
- | Use_assumption
_Luke -> sprintf "<assumption />"
- | Use_contradiction_Luke -> sprintf "<contradiction />"
- | Use_exists_Luke -> sprintf "<exists />"
- | Use_split_Luke -> sprintf "<split />"
- | Use_left_Luke -> sprintf "<left />"
- | Use_right_Luke -> sprintf "<right />"
- | Use_apply
_Luke term -> sprintf "<apply>%s</apply>" term
+ | Use_ring -> sprintf "<ring />"
+ | Use_fourier -> sprintf "<fourier />"
+ | Use_reflexivity -> sprintf "<reflexivity />"
+ | Use_symmetry -> sprintf "<symmetry />"
+ | Use_assumption -> sprintf "<assumption />"
+ | Use_contradiction -> sprintf "<contradiction />"
+ | Use_exists -> sprintf "<exists />"
+ | Use_split -> sprintf "<split />"
+ | Use_left -> sprintf "<left />"
+ | Use_right -> sprintf "<right />"
+ | Use_apply term -> sprintf "<apply>%s</apply>" term
| Hints hints ->
sprintf "<hints>\n%s\n</hints>"
(String.concat "\n" (List.map pp_hint hints))
type hint =
(* tactics usage related hints *)
- | Use_ring_Luke
- | Use_fourier_Luke
- | Use_reflexivity_Luke
- | Use_symmetry_Luke
- | Use_assumption_Luke
- | Use_contradiction_Luke
- | Use_exists_Luke
- | Use_split_Luke
- | Use_left_Luke
- | Use_right_Luke
- | Use_apply_Luke of string (* use apply tactic on embedded term *)
+ | Use_ring
+ | Use_fourier
+ | Use_reflexivity
+ | Use_symmetry
+ | Use_assumption
+ | Use_contradiction
+ | Use_exists
+ | Use_split
+ | Use_left
+ | Use_right
+ | Use_apply of string (* use apply tactic on embedded term *)
(* hints list *)
| Hints of hint list
if uris = [] then
Sorry
else
- Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
+ Eureka (Hints (List.map (fun uri -> Use_apply uri) uris))
with Empty_must -> Sorry
in
let answer = Musing_completed (my_own_id, musing_id, hint) in
in
mk_tactic tac
-
(**
naive implementation of ORELSE tactical, try a sequence of tactics in turn:
if one fails pass to the next one and so on, eventually raises (failure "no
in
mk_tactic (then_ ~start ~continuation)
-(* Galla *)
-(* si suppone che tutte le tattiche sollevino solamente Fail? *)
-
+let rec seq ~tactics =
+ match tactics with
+ | [] -> assert false
+ | [tac] -> tac
+ | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
mk_tactic (try_tactic ~tactic)
;;
+let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
(* This tries tactics until one of them doesn't _solve_ the goal *)
(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
start: ProofEngineTypes.tactic ->
continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+ (** "folding" of then_ *)
+val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
val repeat_tactic:
tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
val solve_tactics:
tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
-
+val fail: ProofEngineTypes.tactic
(*
val prova_tac : ProofEngineTypes.tactic
let fold = ReductionTactics.fold_tac
let fourier = FourierR.fourier_tac
let generalize = VariousTactics.generalize_tac
+let set_goal = VariousTactics.set_goal
let injection = DiscriminationTactics.injection_tac
let intros = PrimitiveTactics.intros_tac
let left = IntroductionTactics.left_tac
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term list -> ProofEngineTypes.tactic
+val set_goal : int -> ProofEngineTypes.tactic
val injection : term:Cic.term -> ProofEngineTypes.tactic
val intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
;;
+let set_goal n =
+ ProofEngineTypes.mk_tactic
+ (fun (proof, goal) ->
+ let (_, metasenv, _, _) = proof in
+ if CicUtil.exists_meta n metasenv then
+ (proof, [n])
+ else
+ raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))
exception AllSelectedTermsMustBeConvertible;;
val assumption_tac: ProofEngineTypes.tactic
+
val generalize_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
ProofEngineTypes.tactic
+ (* change the current goal to those referred by the given meta number *)
+val set_goal: int -> ProofEngineTypes.tactic
uri1 == uri2
;;
+
let string_of_uri uri =
match uri.(Array.length uri - 1) with
| "" ->
| _ ->
String.concat "#"
[ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+
+
let name_of_uri uri = uri.(Array.length uri - 2);;
let buri_of_uri uri = uri.(Array.length uri - 4);;
let depth_of_uri uri = Array.length uri - 3;;
| [t] -> str ^ xp t ^ ")"
| t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"
+let compare u1 u2 =
+ let su1 = string_of_uri u1 in
+ let su2 = string_of_uri u2 in
+ Pervasives.compare su1 su2
+
+module OrderedUri =
+struct
+ type t = uri
+ let compare = compare (* the one above, not Pervasives.compare *)
+end
+
+module UriSet = Set.Make (OrderedUri)
+
type uri
val eq : uri -> uri -> bool
+val compare : uri -> uri -> int
val uri_of_string : string -> uri
type uriref = uri * (int list)
val string_of_uriref : uriref -> string
+module UriSet: Set.S with type elt = uri
+
projects / helm.git / commitdiff